Universal properties for universal types in bifibrational parametricity

DOI10.1017/S0960129518000336zbMath1422.68032OpenAlexW2922774582WikidataQ128207158 ScholiaQ128207158MaRDI QIDQ5377699

Federico Orsanigo, Neil Ghani, Fredrik Nordvall Forsberg

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

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

Related Items (1)

What should a generic object be?

Cites Work

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

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