The Psyche prover

The Ψ project

Dr Stéphane Graham-Lengrand

Chargé de Recherche au CNRS
Professeur Chargé de Cours à l'École Polytechnique

Habilitation à Diriger des Recherches (HDR)

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


Wednesday 17th December 2014 at 14:00
Gilles Kahn room
Alan Turing building, Ecole Polytechnique.


before a panel consisting of
- Wolfgang Ahrendt (rapporteur),
- Hugo Herbelin (rapporteur),
- Frank Pfenning (rapporteur),
- Sylvain Conchon
- David Delahaye
- Didier Galmiche
- Laurent Regnier
- Christine Paulin


The current file: Main.pdf

Coq proofs for Part II

Chapter 4: Subsumed by Chapter 5

Chapter 5:

  • LAF system (with quantifiers): LAF.v
Chapter 6:
  • Realisability models and Adequacy Lemma: Semantics.v
  • LAF system with Eigenvariables: LAFwE.v
  • Realisability models with Eigenvariables and Adequacy Lemma: SemanticswE.v
Chapter 7:

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