Realisability semantics of parametric polymorphism, general references and recursive types

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)

zbMATH Keywords

semantic types

Mathematics Subject Classification ID

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