2026-07-26T10:47:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4212 2024-03-06T10:34:54Z ddc:004 open_access

Internalizing Relational Parametricity in the Extensional Calculus of Constructions Krishnaswami, Neelakantan R. Dreyer, Derek Relational parametricity dependent types quasi-PERs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Neelakantan R. Krishnaswami and Derek Dreyer 2013 Is Part Of LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2013.432 urn:nbn:de:0030-drops-42125 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.432 eng https://creativecommons.org/licenses/by/3.0/legalcode