Relational Parametricity for Higher Kinds

Atkey, Robert

doi:10.4230/LIPIcs.CSL.2012.46

Document

Relational Parametricity for Higher Kinds

Author Robert Atkey

Part of: Volume: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (CSL 2012)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Computer Science Logic (CSL)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2012-09-03

PDF

File

PDF

LIPIcs.CSL.2012.46.pdf

Filesize: 477 kB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CSL.2012.46
URN: urn:nbn:de:0030-drops-36638

Subject Classification

Keywords

Relational Parametricity
Higher Kinds
Polymorphism

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Robert Atkey. Relational Parametricity for Higher Kinds. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 46-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) https://doi.org/10.4230/LIPIcs.CSL.2012.46

Author Details

Robert Atkey

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail