Projects per year
Reynolds' theory of parametric polymorphism captures the invariance of polymorphically typed programs under change of data representation. Semantically, reflexive graph categories and fibrations are both known to give a categorical understanding of parametric polymorphism. This paper contributes further to this categorical perspective by showing the relevance of bifibrations. We develop a bifibrational framework for models of System F that are parametric, in that they verify the Identity Extension Lemma and Reynolds' Abstraction Theorem. We also prove that our models satisfy expected properties, such as the existence of initial algebras and final coalgebras, and that parametricity implies dinaturality.
|Number of pages||17|
|Journal||Electronic Notes in Theoretical Computer Science|
|Publication status||Published - 21 Dec 2015|
|Event||31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI) - Radboud University, Nijmegen, Netherlands|
Duration: 22 Jun 2015 → 25 Jun 2015
- fibred category theory
- logical relations
- system F
FingerprintDive into the research topics of 'Bifibrational functorial semantics of parametric polymorphism'. Together they form a unique fingerprint.
- 2 Finished
1/04/15 → 30/09/19
30/09/13 → 29/09/17