Bifibrational functorial semantics of parametric polymorphism

DOI10.1016/j.entcs.2015.12.011zbMath1351.68072OpenAlexW2204984881WikidataQ113317730 ScholiaQ113317730MaRDI QIDQ5971398

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

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.011

zbMATH Keywords

logical relationsparametricitySystem Ffibred category theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Unnamed Item ⋮ Proof-Relevant Parametricity ⋮ Parametric Polymorphism — Universally ⋮ Universal properties for universal types in bifibrational parametricity ⋮ Parametricity for primitive nested types ⋮ Comprehensive Parametric Polymorphism: Categorical Models and Type Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• Functorial polymorphism
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• Categorical logic and type theory
• Parametricity as isomorphism
• Fundamental concepts in programming languages
• Nominal Sets
• Parametric Polymorphism — Universally
• The impact of higher-order state and control effects on local relational reasoning
• Constructive complete distributivity. I
• Categorical semantics for higher order polymorphic lambda calculus
• Constructive natural deduction and its ‘ω-set’ interpretation
• Categorical data types in parametric polymorphism
• Parametricity and local variables
• State-dependent representation independence
• A kripke logical relation between ML and assembly
• Categorical models for Abadi and Plotkin's logic for parametricity

This page was built for publication: Bifibrational functorial semantics of parametric polymorphism