Habilitation à Diriger des Recherches (HDR)

"Polarities and Focussing: a journey from Realisability to Automated Reasoning"

Defence:

The jury consisted of
- Wolfgang Ahrendt (rapporteur),
- Hugo Herbelin (rapporteur),
- Frank Pfenning (rapporteur),
- Sylvain Conchon
- David Delahaye
- Didier Galmiche
- Laurent Regnier
- Christine Paulin

Dissertation:

Coq proofs for Part II

• Base file: Basic.v

Chapter 5:

• LAF system (with quantifiers): LAF.v

• Realisability models and Adequacy Lemma: Semantics.v
• LAF system with Eigenvariables: LAFwE.v
• Realisability models with Eigenvariables and Adequacy Lemma: SemanticswE.v

• Normalisation theory: NormalisationTheory.v
• Abstract Machines and Head normalisation: HeadReduction.v
• LAF system with Explicit Label Updates, renamings: LAFwEL.v
• Deriving properties from Non-empty realisability models: SemanticsNE.v

All the files for the version with quantifiers: First-order.tar.gz