Cyril Cohen

PhD Thesis

• Home Page
• Scientific work
• Papers and Talks
• PhD Thesis
  • Summary
  • Résumé
• Teaching
• Links

My defence took place on Tuesday November 20, 2012 at 2 p.m. in amphitheatre Monge in “École polytechnique”, with the following jury:

• Assia Mahboubi et Benjamin Werner (Directeurs)
• Jeremy Avigad, Jean-Christophe Filliâtre et Marie-Françoise Roy (Rapporteurs)
• Gilles Barthe, Georges Gonthier et Bas Spitters (Examinateurs)

Thesis

Here is the final version, and the BibTex.
Summary here / Résumé ici.

Coq Source code

Here is the Coq source code for the formalizations described in my thesis, you need ssreflect to compile it. Note that some files are in the 1.4 release of ssreflect (ssrnum.v, ssrint.v, rat.v, generic_quotient.v). If something is missing, please tell me.
These sources contain:

• 18605 lines of code
• 978 Definitions, Inductive types and Canonical Structures
• 1951 Lemmas, Facts and Theorems

---