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)
- Institution
- Appalachian State University (ASU )
- Web Site: https://library.appstate.edu/
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.
Bifibrational Functorial Semantics For Parametric Polymorphism
PDF (Portable Document Format)
412 KB
Created on 8/8/2016
Views: 426
Additional Information
- Publication
- 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 www.sciencedirect.com
- Language: English
- Date: 2015
- Keywords
- Parametricity, Logical relations, System F, Fibred Category Theory