Advertisement

Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types

  • Lars Birkedal
  • Kristian Støvring
  • Jacob Thamsborg
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)

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.

Keywords

General Reference Operational Semantic Semantic Type Recursive Equation Ultrametric Space 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 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. 2.
    Ahmed, A.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)Google Scholar
  3. 3.
    Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of POPL (to appear, 2009)Google Scholar
  4. 4.
    Amadio, R.M.: Recursion over realizability structures. Information and Computation 91(1), 55–85 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  6. 6.
    America, P., Rutten, J.J.M.M.: Solving reflexive domain equations in a category of complete metric spaces. J. Comput. Syst. Sci. 39(3), 343–375 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 86–101. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Birkedal, L., Støvring, K., Thamsborg, J.: Relational parametricity for references and recursive types. In: Proceedings of TLDI (to appear, 2009)Google Scholar
  9. 9.
    Bohr, N., Birkedal, L.: Relational reasoning for recursive types and references. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 79–96. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Cardone, F.: Relational semantics for recursive types and bounded quantification. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 164–178. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  11. 11.
    Crary, K., Harper, R.: Syntactic logical relations for polymorphic and recursive types. Electronic Notes in Theoretical Computer Science 172, 259–299 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Levy, P.B.: Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation 19(4), 377–414 (2006)CrossRefzbMATHGoogle Scholar
  13. 13.
    MacQueen, D.B., Plotkin, G.D., Sethi, R.: An ideal model for recursive polymorphic types. Information and Control 71(1/2), 95–130 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)Google Scholar
  15. 15.
    Moggi, E.: Notions of computation and monads. Information and Computation 93, 55–92 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Petersen, R.L., Birkedal, L., Nanevski, A., Morrisett, G.: A realizability model for impredicative hoare type theory. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 337–352. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  18. 18.
    Pitts, A.M.: Relational properties of domains. Information and Computation 127, 66–90 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Plotkin, G.D., Power, J.: Computational effects and operations: An overview. Electronic Notes in Theoretical Computer Science 73, 149–163 (2004)CrossRefzbMATHGoogle Scholar
  20. 20.
    Rutten, J.J.M.M.: Elements of generalized ultrametric domain theory. Theoretical Computer Science 170(1-2), 349–381 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM Journal on Computing 11(4), 761–783 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Wagner, K.R.: Solving Recursive Domain Equations with Enriched Categories. PhD thesis, Carnegie Mellon University (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Lars Birkedal
    • 1
  • Kristian Støvring
    • 1
  • Jacob Thamsborg
    • 1
  1. 1.IT University of CopenhagenCopenhagen SDenmark

Personalised recommendations