The next 700 syntactical models of type theory

Abstract : A family of syntactic models for the calculus of construction with universes (CC ω) is described, all of them preserving conversion of the calculus definitionally, and thus giving rise directly to a program transformation of CC ω into itself. Those models are based on the remark that negative type constructors (e.g., dependent product, coinductive types or universes) are underspecified in type theory—which leaves some freedom on extra intensional specifications. The model construction can be seen as a compilation phase from a complex type theory into a simpler type theory. Such models can be used to derive (the negative part of) independence results with respect to CC ω , such as functional extensional-ity, propositional extensionality, univalence or the fact that bisimulation on a coinductive type may not coincide with equality. They can also be used to add new principles to the theory, which we illustrate by defining a version of CC ω with ad-hoc polymorphism that shows in particular that para-metricity is not an implicit requirement of type theory. The correctness of some of the models/program transformations have been checked in the COQ proof assistant and have been instrumented as a COQ plugin.
Type de document :
Communication dans un congrès
Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.182 - 194, 2017, <10.1145/3018610.3018620>
Liste complète des métadonnées
Contributeur : Nicolas Tabareau <>
Soumis le : mercredi 25 janvier 2017 - 13:20:20
Dernière modification le : jeudi 15 juin 2017 - 09:08:56


Fichiers produits par l'(les) auteur(s)




Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau. The next 700 syntactical models of type theory. Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.182 - 194, 2017, <10.1145/3018610.3018620>. <hal-01445835>



Consultations de
la notice


Téléchargements du document