Universal properties for universal types in bifibrational parametricity

DOI10.1017/S0960129518000336zbMATH Open1422.68032OpenAlexW2922774582WikidataQ128207158 ScholiaQ128207158MaRDI QIDQ5377699FDOQ5377699

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

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

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)

Cites Work

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

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)