The next 700 syntactical models of type theory
Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau · 2016
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.