Bifibrational functorial semantics of parametric polymorphism

Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, Tim Revell

Research output: Contribution to journalArticle

2 Citations (Scopus)
99 Downloads (Pure)

Abstract

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.

Original languageEnglish
Pages (from-to)165-181
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Volume319
DOIs
Publication statusPublished - 21 Dec 2015
Event31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI) - Radboud University, Nijmegen, Netherlands
Duration: 22 Jun 201525 Jun 2015

Keywords

  • fibred category theory
  • logical relations
  • parametricity
  • system F

Fingerprint Dive into the research topics of 'Bifibrational functorial semantics of parametric polymorphism'. Together they form a unique fingerprint.

Cite this