Bifibrational Functorial Semantics For Parametric Polymorphism

ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
Patricia Johann Ph.D, Professor (Creator)
Appalachian State University (ASU )
Web Site:

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.

Additional Information

Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, and Tim Revell.(2015) "Bifibrational Functorial Semantics for Parametric Polymorphism". Mathematical Foundations of Program Semantics (MFPS'15), pp. 165-181. Version Of Record Available At
Language: English
Date: 2015
Parametricity, Logical relations, System F, Fibred Category Theory

Email this document to