Universal properties for universal types in bifibrational parametricity

DOI10.1017/S0960129518000336MaRDI QIDQ5377699zbMATH OpenOpenAlexWikidataFDO

Authors Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo

Publication date 27 May 2019

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129518000336

zbMATH Keywords

categorical semanticsrelational parametricitycomprehension categories

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Categorical semantics of formal languages (18C50)

Recommendations

• Parametric Polymorphism — Universally
• Bifibrational functorial semantics of parametric polymorphism
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• Formal parametric polymorphism
• A relationally parametric model of dependent type theory

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 3882404 (Why is no real title available?)
• scientific article; zbMATH DE number 4049849 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 512792 (Why is no real title available?)
• scientific article; zbMATH DE number 3370546 (Why is no real title available?)
• A Kripke logical relation between ML and assembly
• Bifibrational functorial semantics of parametric polymorphism
• Categorical logic and type theory
• Categorical models for Abadi and Plotkin's logic for parametricity
• Categorical semantics for higher order polymorphic lambda calculus
• Comprehension categories and the semantics of type dependency
• Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
• Fundamental concepts in programming languages
• Parametric Polymorphism — Universally
• Proof-Relevant Parametricity
• State-dependent representation independence
• The calculus of constructions
• The impact of higher-order state and control effects on local relational reasoning
• Translating dependency into parametricity
• Typed closure conversion preserves observational equivalence

Cited in

(3)

• What should a generic object be?
• Core algebra revisited
• Bifibrational functorial semantics of parametric polymorphism

This page was built for publication: Universal properties for universal types in bifibrational parametricity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5377699)