Séminaire du Laboratoire Spécification et Vérification avec Bruno Barras
Le mardi 28 mars 2017 à 11h00 aura lieu un séminaire organisé par le Laboratoire Spécification et Vérification (LSV) de l'ENS Paris-Saclay.
Bruno Barras (École polytechnique - Laboratoire d'Informatique de l'École polytechnique) fera un exposé intitulé "A formal set-theoretical model of Coq and its application to strong normalization".
- Date : 28/03/2017
- Lieu : Bâtiment Institut D'Alembert - Auditorium Daniel Chemla
Bruno Barras, Ecole polytechnique - Laboratoire d'Informatique de l'Ecole polytechnique
"A formal set-theoretical model of Coq and its application to strong normalization"
I will describe the formalization in Coq of two crucial metatheoretical properties of the formalism of the Coq proof assistant: consistency and
strong normalization (SN). While it is clear why we prove the consistency of a logical formalism, I will give a motivation for the SN property.
Of course, as Gödel showed, proving the consistency of a formalism in itself is only proving it is inconsistent. The usual way out is to make Coq stronger by adding axioms. In our case, we have extended Coq to make it as strong as intuitionistic set-theory with Grothendieck universes (an intuitionistic counterpart of inaccessible cardinals).
Then, I will sketch an intuitive translation from the Calculus of Inductive Constructions (the formalism of Coq) to set theory, and prove that this interpretation is sound. The difficult part is to interpret inductive types. As a reward, we derive the consistency of Coq relative to the set theory described above.
Using a slight variant of the set-theoretical interpretation, I will explain how to build a strong normalization model, which soundness implies the SN property. The remarkable feature of this model is that it is very modular: the complexity of inductive types have been broken into simpler principles.