Logical relations and parametricity -- a Reynolds programme for category theory and programming languages

DOI10.1016/j.entcs.2014.02.008zbMath1337.68052OpenAlexW2006850413WikidataQ113317888 ScholiaQ113317888MaRDI QIDQ280200

Uday S. Reddy, Edmund P. Robinson, Claudio Hermida

Publication date: 6 May 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2014.02.008

zbMATH Keywords

homomorphismsfibrationscategory theorydefinabilityuniversal algebrainformation hidingreflexive graphsrelational parametricitydata abstractionlogical relationsnatural transformationsparametric polymorphismrelation lifting

Mathematics Subject Classification ID

Theory of programming languages (68N15) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Deriving logical relations from interpretations of predicate logic, Relation lifting, a survey, Bisimulation as a logical relation, Unnamed Item, Bifibrational functorial semantics of parametric polymorphism, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, Comprehensive Parametric Polymorphism: Categorical Models and Type Theory, Pointers in Recursion: Exploring the Tropics, Towards a Cubical Type Theory without an Interval

Cites Work

• Foundations of algebraic specification and formal software development.
• A categorical outlook on relational modalities and simulations
• Core algebra revisited
• Structural induction and coinduction in a fibrational setting
• Categorical logic and type theory
• 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
• Relation lifting, with an application to the many-valued cover modality
• Logical relations and the typed λ-calculus
• Parametricity and local variables
• Data Refinement
• Catégories structurées
• Products of Automata and the Problem of Covering
• Categorical models for Abadi and Plotkin's logic for parametricity
• General Theory of Natural Equivalences
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item