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

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

Lars Birkedal, Kristian Støvring, Jacob Thamsborg

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

68N15: Theory of programming languages

68Q65: Abstract data types; algebraic specification

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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