Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
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.
KeywordsGeneral Reference Operational Semantic Semantic Type Recursive Equation Ultrametric Space
- 1.Abadi, M., Plotkin, G.D.: A per model of polymorphism and recursive types. In: Proceedings of LICS, pp. 355–365 (1990)Google Scholar
- 2.Ahmed, A.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)Google Scholar
- 3.Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of POPL (to appear, 2009)Google Scholar
- 8.Birkedal, L., Støvring, K., Thamsborg, J.: Relational parametricity for references and recursive types. In: Proceedings of TLDI (to appear, 2009)Google Scholar
- 14.Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)Google Scholar
- 22.Wagner, K.R.: Solving Recursive Domain Equations with Enriched Categories. PhD thesis, Carnegie Mellon University (1994)Google Scholar