Home

Publications

Github

Teaching (old)

Dr Stéphane Graham-Lengrand

Senior Computer Scientist at SRI International
Computer Science Laboratory
Formal Methods group

SRI International
333, Ravenswood Avenue
Menlo Park, California 94025, USA

Office:
Telephone: +1 (650) 859-2000
e-mail

Habilitation à Diriger des Recherches (HDR)

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

Defence:

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

Access

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

Dissertation:

See: https://hal.archives-ouvertes.fr/tel-01094980

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