Sites Inria

English version

Séminaire des équipes de recherche

Coinduction all the way up

© INRIA Sophie Auvin - G comme Grille

  • Date : 12/09/2016
  • Lieu : 2 rue Simone Iff, 75012 Paris - Salle Jacques-Louis Lions 1, bâtiment C - 10h30
  • Intervenant(s) : Damien Pous

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 conduction, 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.

Mots-clés : Way up Conduction Gallium Séminaire

Haut de page

Suivez Inria