Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Nicolas Tabareau Connect in order to contact the contributor
Submitted on : Wednesday, January 25, 2017 - 1:20:20 PM
Last modification on : Friday, January 21, 2022 - 3:20:27 AM


Files produced by the author(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, ⟨10.1145/3018610.3018620⟩. ⟨hal-01445835⟩



Les métriques sont temporairement indisponibles