Internalizing Relational Parametricity in the Extensional Calculus of Constructions

Authors Neelakantan R. Krishnaswami, Derek Dreyer

Thumbnail PDF


  • Filesize: 0.56 MB
  • 20 pages

Document Identifiers

Author Details

Neelakantan R. Krishnaswami
Derek Dreyer

Cite AsGet BibTex

Neelakantan R. Krishnaswami and Derek Dreyer. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 432-451, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


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 different ways. Using our model, we can validate the soundness of quotient types, as well as derive strong equality axioms for Church-encoded data, such as the usual induction principles for Church naturals and booleans, and the eta law for strong dependent pair types. Furthermore, we show that such equivalences, justified by relationally parametric reasoning, may soundly be internalized (i.e., added as equality axioms to our type theory). Thus, we demonstrate that it is possible to interpret equality in a dependently-typed setting using parametricity. The key idea behind our approach is to interpret types as so-called quasi-PERs (or zigzag-complete relations), which enable us to model the symmetry and transitivity of equality while at the same time allowing abstract types with different representations to be equated.
  • Relational parametricity
  • dependent types
  • quasi-PERs


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads