Tuesday 30 May 2017, 14:00: Models of type theory given by program translation, Simon Boulier (EPI Ascola, Nantes).
I will present the results of the article "The next 700 syntactical
models of type theory" (CPP 2017).
This article propose several simple models of the Calculus of Constructions with universes (CCω) given by program translation. Such models can be seen as the compilation from an involved type theory to a simpler type theory.
We use this technique to show easily that some axioms are not derivable in CCω: functional extensionality, propositional extensionality, and the fact that bisimulation does not imply equality for streams. Those models also allows to add new operators in the source theory. We take the example of the pattern-matching on a universe. I will make a demo of our implementation of several translations as Coq plug-ins.