PhD thesis of David Baelde
A linear approach to the proof-theory of
least and greatest fixed points
Sous la direction de Dale Miller.
Manuscript (in english): defense version (PDF).
Jury
- Patrick Baillot (Rapporteur)
- Gilles Dowek
- Olivier Laurent
- Paul-André Melliès
- Dale Miller (Directeur de thèse)
- Gopalan Nadathur
- Christine Paulin-Mohring (Rapporteur)
- Frank Pfenning (Rapporteur)
Abstract
Least and greatest fixed point constructions are associated to the concepts of inductive and coinductive definitions, and the deductive principles of induction and coinduction. We study the proof theory of these concepts, in the simplifying framework of linear logic, where the duality between least and greatest fixed points is fully expressed. An essential aspect of fixed point constructions is that they yield structured infinities. That structure, captured in the logic, allows to derive some interesting properties: contraction and weakening are admissible for some formulas; similarly, we derive structural properties of generic quantification (nabla), reformulated to interact well with fixed points. The core of the thesis is the extension of focusing to fixed points. Focusing is a fundamental property of the structure of proofs, used in game semantics as well as in proof-search. We show that our focusing discipline extends well to the intuitionistic setting, and apply them to automated (co)inductive theorem proving.
