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 metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01445835
Contributor : Nicolas Tabareau <>
Submitted on : Wednesday, January 25, 2017 - 1:20:20 PM
Last modification on : Tuesday, March 26, 2019 - 9:25:22 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

1513

Files downloads

609