Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types

DOI10.1007/978-3-642-00596-1_32zbMath1234.68052OpenAlexW203992540MaRDI QIDQ3617747

Jacob Thamsborg, Kristian Støvring, Lars Birkedal

Publication date: 31 March 2009

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-00596-1_32

Mathematics Subject Classification ID

Theory of programming languages (68N15) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

A Kripke logical relation for effect-based program transformations ⋮ The category-theoretic solution of recursive metric-space equations ⋮ A relational realizability model for higher-order stateful ADTs ⋮ Weak updates and separation logic ⋮ Nested Hoare Triples and Frame Rules for Higher-Order Store ⋮ A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Elements of generalized ultrametric domain theory
• Solving reflexive domain equations in a category of complete metric spaces
• Notions of computation and monads
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Recursion over realizability structures
• Relational properties of domains
• Syntactic Logical Relations for Polymorphic and Recursive Types
• Realisability semantics of parametric polymorphism, general references and recursive types
• An ideal model for recursive polymorphic types
• The Category-Theoretic Solution of Recursive Domain Equations
• State-dependent representation independence
• Relational Reasoning for Recursive Types and References
• A Realizability Model for Impredicative Hoare Type Theory
• Typed Lambda Calculi and Applications

This page was built for publication: Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types