Presenter: Linyu Yang
Author: Damien Pous
Abstract: 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 parameterized 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 a historical peculiarity about upto 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.