A Relationally Parametric Model of the Calculus of Constructions

Derek and I have a new paper out, on a new parametric model of the calculus of constructions. A Relationally Parametric Model of the Calculus of Constructions

In this paper, we give the first relationally parametric model of the (extensional) calculus of constructions. Our model remains as simple as traditional PER models of dependent types, but unlike them, our model additionally permits relating terms at different implementation types. Using this model, we can validate the soundness of quotient types, as well as derive strong equality axioms for Church-encoded data, such as the eta-law for strong dependent pair types.

Insofar as anything having to do with dependent types can be, the key idea in this paper is really, really simple. There's a really beautiful, simple generalization of partial equivalence relations (aka PERs) (called quasi-PERs) that let us give a parametric model without having to jump through the hoops the usual methods does.