Realisability semantics of parametric polymorphism, general references and recursive types
From MaRDI portal
Publication:3583027
DOI10.1017/S0960129510000162zbMath1209.68122MaRDI QIDQ3583027
Kristian Støvring, Jacob Thamsborg, Lars Birkedal
Publication date: 26 August 2010
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (9)
A Kripke logical relation for effect-based program transformations ⋮ Specification patterns for reasoning about recursion through the store ⋮ A relational realizability model for higher-order stateful ADTs ⋮ Program equivalence in a simple language with state ⋮ Partiality, State and Dependent Types ⋮ Syntactic soundness proof of a type-and-capability system with hidden state ⋮ Step-Indexed Kripke Model of Separation Logic for Storable Locks ⋮ Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types ⋮ Realizability models for a linear dependent PCF
Cites Work
- 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
- The connection between initial and unique solutions of domain equations in the partial order and metric approach
- A game semantics for generic polymorphism
- Games and full abstraction for FPC.
- Relational properties of domains
- Syntactic Logical Relations for Polymorphic and Recursive Types
- A Semantic Foundation for Hidden State
- Nested Hoare Triples and Frame Rules for Higher-Order Store
- An ideal model for recursive polymorphic types
- The Category-Theoretic Solution of Recursive Domain Equations
- [top [top ]-closed relations and admissibility]
- Relational Reasoning for Recursive Types and References
- A Fully Abstract Trace Semantics for General References
- A Realizability Model for Impredicative Hoare Type Theory
This page was built for publication: Realisability semantics of parametric polymorphism, general references and recursive types
