Picture of neon light reading 'Open'

Discover open research at Strathprints as part of International Open Access Week!

23-29 October 2017 is International Open Access Week. The Strathprints institutional repository is a digital archive of Open Access research outputs, all produced by University of Strathclyde researchers.

Explore recent world leading Open Access research content this Open Access Week from across Strathclyde's many research active faculties: Engineering, Science, Humanities, Arts & Social Sciences and Strathclyde Business School.

Explore all Strathclyde Open Access research outputs...

Strathprints

Relational parametricity for higher kinds

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

[img]
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.

Item type: Book Section
ID code: 40756
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 2017 09:06
Related URLs:
URI: https://strathprints.strath.ac.uk/id/eprint/40756
Export data:
CORE (COnnecting REpositories)