Internalizing Relational Parametricity in the Extensional Calculus of Constructions

摘要

We give the first relationally parametric model of the extensional calculus of constructions. Our model remains as simple as traditional PER models of types, but unlike them, it additionally permits the relating of terms that implement abstract types in d