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.