Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
| Autor: | Lars Birkedal, Jacob Thamsborg, Kristian Støvring |
|---|---|
| Rok vydání: | 2009 |
| Předmět: | |
| Zdroj: | Foundations of Software Science and Computational Structures ISBN: 9783642005954 FoSSaCS |
| DOI: | 10.1007/978-3-642-00596-1_32 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|