Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
DOI10.1016/J.ENTCS.2014.02.008zbMATH Open1337.68052OpenAlexW2006850413WikidataQ113317888 ScholiaQ113317888MaRDI QIDQ280200FDOQ280200
Authors: Claudio Hermida, Uday S. Reddy, Edmund P. Robinson 
Publication date: 6 May 2016
Full work available at URL: https://doi.org/10.1016/j.entcs.2014.02.008
Recommendations
category theoryinformation hidingreflexive graphsrelational parametricitydefinabilitydata abstractionfibrationshomomorphismslogical relationsnatural transformationsparametric polymorphismrelation liftinguniversal algebra
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Structural induction and coinduction in a fibrational setting
- Categorical logic and type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Parametricity and local variables
- Data Refinement
- Title not available (Why is that?)
- Title not available (Why is that?)
- Some properties of Fib as a fibred \(2\)-category
- Fundamental concepts in programming languages
- Relational properties of domains
- Closed systems of functions and predicates
- Proof of correctness of data representations
- Title not available (Why is that?)
- Relation lifting, with an application to the many-valued cover modality
- Title not available (Why is that?)
- Logical relations and the typed λ-calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Catégories structurées
- Products of Automata and the Problem of Covering
- Title not available (Why is that?)
- Categorical models for Abadi and Plotkin's logic for parametricity
- General Theory of Natural Equivalences
- Foundations of algebraic specification and formal software development.
- A categorical outlook on relational modalities and simulations
- Core algebra revisited
Cited In (18)
- Types, abstraction, and parametric polymorphism, part 2
- A fibrational tale of operational logical relations: pure, effectful and differential
- Title not available (Why is that?)
- Relation lifting, a survey
- Deriving logical relations from interpretations of predicate logic
- POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE
- Title not available (Why is that?)
- Bisimulation as a logical relation
- Intensional harmony as isomorphism
- Non-parametric parametricity
- Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
- Relational limits in general polymorphism
- Bifibrational functorial semantics of parametric polymorphism
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
- Logical predicates in higher-order mathematical operational semantics
- Parametricity as isomorphism
- Towards a Cubical Type Theory without an Interval
- Pointers in Recursion: Exploring the Tropics
This page was built for publication: Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q280200)
