Categorical models for Abadi and Plotkin's logic for parametricity

DOI10.1017/S0960129505004834zbMath1082.03012OpenAlexW2018103337MaRDI QIDQ5697712

Rasmus Ejlers Møgelberg, Lars Birkedal

Publication date: 18 October 2005

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

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

zbMATH Keywords

categorical modelsrelational parametricitysecond-order \(\lambda\)-calculusAPL-structure

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Combinatory logic and lambda calculus (03B40)

Related Items

Logical relations and parametricity -- a Reynolds programme for category theory and programming languages ⋮ A fibrational framework for possible-world semantics of \textsc{Algol}-like languages ⋮ Parametric Polymorphism — Universally ⋮ Universal properties for universal types in bifibrational parametricity ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ Unnamed Item ⋮ Parametricity for primitive nested types ⋮ Synthetic domain theory and models of linear Abadi {\&} Plotkin logic ⋮ HasCasl: integrated higher-order specification and program development ⋮ Comprehensive Parametric Polymorphism: Categorical Models and Type Theory ⋮ From parametric polymorphism to models of polymorphic FPC ⋮ Relational Parametricity for Control Considered as a Computational Effect