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.
Chapter PDF
Similar content being viewed by others
Keywords
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
Abadi, M., Plotkin, G.D.: A per model of polymorphism and recursive types. In: Proceedings of LICS, pp. 355–365 (1990)
Ahmed, A.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)
Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of POPL (to appear, 2009)
Amadio, R.M.: Recursion over realizability structures. Information and Computation 91(1), 55–85 (1991)
Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge University Press, Cambridge (1998)
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)
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)
Birkedal, L., Støvring, K., Thamsborg, J.: Relational parametricity for references and recursive types. In: Proceedings of TLDI (to appear, 2009)
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)
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)
Crary, K., Harper, R.: Syntactic logical relations for polymorphic and recursive types. Electronic Notes in Theoretical Computer Science 172, 259–299 (2007)
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)
MacQueen, D.B., Plotkin, G.D., Sethi, R.: An ideal model for recursive polymorphic types. Information and Control 71(1/2), 95–130 (1986)
Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)
Moggi, E.: Notions of computation and monads. Information and Computation 93, 55–92 (1991)
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)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Pitts, A.M.: Relational properties of domains. Information and Computation 127, 66–90 (1996)
Plotkin, G.D., Power, J.: Computational effects and operations: An overview. Electronic Notes in Theoretical Computer Science 73, 149–163 (2004)
Rutten, J.J.M.M.: Elements of generalized ultrametric domain theory. Theoretical Computer Science 170(1-2), 349–381 (1996)
Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM Journal on Computing 11(4), 761–783 (1982)
Wagner, K.R.: Solving Recursive Domain Equations with Enriched Categories. PhD thesis, Carnegie Mellon University (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Birkedal, L., Støvring, K., Thamsborg, J. (2009). Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types. In: de Alfaro, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2009. Lecture Notes in Computer Science, vol 5504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00596-1_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-00596-1_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00595-4
Online ISBN: 978-3-642-00596-1
eBook Packages: Computer ScienceComputer Science (R0)