Damien Pous' home page

Coinduction All the Way Up

This page is a web appendix the following paper, that appeared in Proc. LICS'16 (free pdf here).


We revisit coinductive proof principles from a lattice theoretic point of view.
By associating to any monotone function a function which we call the companion, we give a new presentation of both Knaster-Tarski's seminal result, and of the more recent theory of enhancements of the coinductive proof method (up-to techniques).
The resulting theory encompasses parametrised coinduction, as recently proposed by Hur et al., and second-order reasoning, i.e., the ability to reason coinductively about the enhancements themselves. It moreover resolves an historical peculiarity about up-to context techniques.
Based on these results, we present an open-ended proof system allowing one to perform proofs on-the-fly and to neatly separate inductive and coinductive phases.

Coq proofs

Most of the paper is formalised in the Coq proof assistant. Only the example about the pi-calculus is not covered.

The library is standalone; each module is documented; links below point to the coqdoc generated documentation. The coqdoc table of contents is here.

Thanks to this new theory, the library is extremely small: coqwc reports 721 lines of specifications, 622 lines of proofs, and 175 lines of comments.


The Coq library is distributed under the terms of the GNU Lesser General Public License version 3.