A relational realizability model for higher-order stateful ADTs

DOI10.1016/J.JLAP.2012.03.004zbMATH Open1279.68227OpenAlexW2166810499MaRDI QIDQ444500FDOQ444500

Authors: Lars Birkedal, Kristian Støvring, Jacob Thamsborg 

Publication date: 14 August 2012

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2012.03.004

Recommendations

• A relational modal logic for higher-order stateful ADTs
• State-dependent representation independence
• A Realizability Model for Impredicative Hoare Type Theory
• The impact of higher-order state and control effects on local relational reasoning
• The impact of higher-order state and control effects on local relational reasoning

zbMATH Keywords

logical relationsparametricityabstract data typeslocal state

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Cites Work

• The Category-Theoretic Solution of Recursive Domain Equations
• Title not available (Why is that?)
• The impact of higher-order state and control effects on local relational reasoning
• State-dependent representation independence
• Notions of computation and monads
• Relational properties of domains
• Title not available (Why is that?)
• Types and programing languages
• Operational reasoning for functions with local state
• Realisability semantics of parametric polymorphism, general references and recursive types
• Solving reflexive domain equations in a category of complete metric spaces
• Processes and the denotational semantics of concurrency
• Semi-metrics, closure spaces and digital topology
• A relational modal logic for higher-order stateful ADTs
• Recursion over realizability structures
• The connection between initial and unique solutions of domain equations in the partial order and metric approach
• A very modal model of a modern, major, general type system
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Title not available (Why is that?)
• Relational Reasoning for Recursive Types and References
• Typed Lambda Calculi and Applications
• Title not available (Why is that?)
• Programming Languages and Systems
• The category-theoretic solution of recursive metric-space equations

Cited In (2)

• A Realizability Model for Impredicative Hoare Type Theory
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types

This page was built for publication: A relational realizability model for higher-order stateful ADTs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q444500)