Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
From MaRDI portal
Publication:3617747
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
68N15: Theory of programming languages
68Q65: Abstract data types; algebraic specification
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
A relational realizability model for higher-order stateful ADTs, The category-theoretic solution of recursive metric-space equations, 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