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.46
URN: urn:nbn:de:0030-drops-36638
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3663/
Go to the corresponding LIPIcs Volume Portal

Atkey, Robert

Relational Parametricity for Higher Kinds

pdf-format:
9.pdf (0.5 MB)

Abstract

Reynolds' notion of relational parametricity has been extremely
influential and well studied for polymorphic programming languages and
type theories based on System F. The extension of relational
parametricity to higher kinded polymorphism, which allows
quantification over type operators as well as types, has not received
as much attention. We present a model of relational parametricity for
System Fomega, within the impredicative Calculus of Inductive
Constructions, and show how it forms an instance of a general class of
models defined by Hasegawa. We investigate some of the consequences of
our model and show that it supports the definition of inductive types,
indexed by an arbitrary kind, and with reasoning principles provided
by initiality.

BibTeX - Entry

@InProceedings{atkey:LIPIcs:2012:3663,
  author =	{Robert Atkey},
  title =	{{Relational Parametricity for Higher Kinds}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{46--61},
  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/3663},
  URN =		{urn:nbn:de:0030-drops-36638},
  doi =		{10.4230/LIPIcs.CSL.2012.46},
  annote =	{Keywords: Relational Parametricity, Higher Kinds, Polymorphism}
}

Keywords: Relational Parametricity, Higher Kinds, Polymorphism
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