License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2012.381
URN: urn:nbn:de:0030-drops-36851
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3685/
Go to the corresponding LIPIcs Volume Portal

Keller, Chantal ; Lasson, Marc

Parametricity in an Impredicative Sort

pdf-format:
31.pdf (0.5 MB)

Abstract

Reynold's abstraction theorem is now a well-established result for a
large class of type systems. We propose here a definition of relational parametricity and a proof of the abstraction theorem in the Calculus of Inductive Constructions (CIC), the underlying formal language of Coq, in which parametricity relations' codomain is the impredicative sort of propositions. To proceed, we need to refine this calculus by splitting the sort hierarchy to separate informative terms from non-informative terms. This refinement is very close to CIC, but with the property that typing judgments can distinguish informative terms. Among many applications, this natural encoding of parametricity inside CIC serves both theoretical purposes (proving the independence of propositions with respect to the logical system) as well as practical aspirations (proving properties of finite algebraic structures). We finally discuss how we can simply build, on top of our calculus, a new reflexive Coq tactic that constructs proof terms by parametricity.

BibTeX - Entry

@InProceedings{keller_et_al:LIPIcs:2012:3685,
  author =	{Chantal Keller and Marc Lasson},
  title =	{{Parametricity in an Impredicative Sort}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{381--395},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{Patrick C{\'e}gielski and Arnaud Durand},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3685},
  URN =		{urn:nbn:de:0030-drops-36851},
  doi =		{10.4230/LIPIcs.CSL.2012.381},
  annote =	{Keywords: Calculus of Inductive Constructions, parametricity, impredicativity, Coq, universes}
}

Keywords: Calculus of Inductive Constructions, parametricity, impredicativity, Coq, universes
Collection: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Issue Date: 2012
Date of publication: 03.09.2012

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