A relational realizability model for higher-order stateful ADTs

DOI10.1016/J.JLAP.2012.03.004MaRDI QIDQ444500zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(5)

• A Realizability Model for Impredicative Hoare Type Theory
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• State-dependent representation independence
• A relational modal logic for higher-order stateful ADTs
• Evidenced frames. A unifying framework broadening realizability models

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)