License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.432
URN: urn:nbn:de:0030-drops-42125
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4212/
Go to the corresponding LIPIcs Volume Portal

Krishnaswami, Neelakantan R. ; Dreyer, Derek

Internalizing Relational Parametricity in the Extensional Calculus of Constructions

pdf-format:
32.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{krishnaswami_et_al:LIPIcs:2013:4212,
  author =	{Neelakantan R. Krishnaswami and Derek Dreyer},
  title =	{{Internalizing Relational Parametricity in the Extensional Calculus of Constructions}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{432--451},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4212},
  URN =		{urn:nbn:de:0030-drops-42125},
  doi =		{10.4230/LIPIcs.CSL.2013.432},
  annote =	{Keywords: Relational parametricity, dependent types, quasi-PERs}
}

Keywords: Relational parametricity, dependent types, quasi-PERs
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI