Paper Info
Title
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
Abstract
We present a realizability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types (as needed for parametricity reasoning) that include general reference types. The interpretation uses a new approach to modeling references. The universe of semantic types consists of world-indexed families of logical relations over a universal predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds. We illustrate how the model can be used to prove simple equivalences between different implementations of imperative abstract data types.
Year
DOI
Venue
2009
10.1007/978-3-642-00596-1_32
Mathematical Structures in Computer Science
Keywords
DocType
Volume
realizability semantics,general reference type,semantic type,relational interpretation,realizability model,logical relation,realisability semantics,recursive type,kripke logical relation,general first-class reference,recursive types,general references,parametric polymorphism,appropriate category,realisability model,recursive equation,modelling reference,indexation,higher order,abstract data type,metric space,programming language
Conference
20
Issue
ISSN
Citations 
4
0302-9743
18
PageRank 
References 
Authors
0.82
25
3
Name
Order
Citations
PageRank
Lars Birkedal1148196.84
Kristian Støvring2646.91
Jacob Thamsborg3725.77