Relational parametricity for higher kinds

Atkey, Robert; (2012) Relational parametricity for higher kinds. In: Computer science logic. EPTCS . UNSPECIFIED. (In Press)

Preview

PDF fomega_parametricity.pdf Download (556kB)| Preview

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 Fω, 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.

ORCID iDs

Atkey, Robert ORCID: https://orcid.org/0000-0002-4414-5047

• Share and Export
  

  RDF+XMLBibTeXRIOXX2 XMLRDF+N-TriplesJSONDublin CoreAtomSimple MetadataReferMETSArchivematicaHTML CitationASCII CitationOpenURL ContextObjectEndNoteOpenURL ContextObject in SpanMODSMPEG-21 DIDLEP3 XMLData Cite XMLRIS (EndNote Online, Zotero, Ref manager, etc)RDF+N3Multiline CSV
• Item metadata

  Item type:	Book Section
  ID code:	40756
  Dates:	Date Event 2012 Published 2012 Accepted
  Keywords:	relational parametricity, polymorphism, higher kinds, polymorphic programming languages, system f, Electronic computers. Computer science
  Subjects:	Science > Mathematics > Electronic computers. Computer science
  Department:	Faculty of Science > Computer and Information Sciences
  Depositing user:	Pure Administrator
  Date deposited:	06 Aug 2012 14:56
  Last modified:	23 Sep 2021 01:17
  Related URLs:	Author
  URI:	https://strathprints.strath.ac.uk/id/eprint/40756