Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 2, bâtiment C

                          Lundi 12 septembre, 10h30

                                 -----------
                                 Damien Pous
                                 -----------

                               CNRS & ENS Lyon

                          ==========================
                          Coinduction all the way up
                          ==========================

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.