Abstract
A game semantic approach to interpreting call-by-value polymorphism is described, based on extending Hyland-Ong games (which have already proved a rich source of models for higher-order programming languages with computational effects) with explicit “copycat links”. This captures universal quantification in a simple and concrete way; it is effectively presentable, and opens the possibility of extending existing model checking techniques to polymorphic types. In particular, we present a fully abstract semantics for a call-by-value language with general references and full higher-rank polymorphism, within which polymorphic objects, for example, may be represented. We prove full abstraction by showing that every universally quantified type is a definable retract of its instantiation with the type of natural numbers.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abramsky, S., Jagadeesan, R.: A game semantics for generic polymorphism. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 1–22. Springer, Heidelberg (2003)
Abramsky, S., Honda, K., McCusker, G.: A fully abstract games semantics for general references. In: Proceedings of the 13th Annual Symposium on Logic in Computer Science, LICS 1998 (1998)
Abramsky, S., Jagadeesan, R.: Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic 59, 543–574 (1994)
Le Botlan, D., Rémy, D.: MLF: Raising ML to the power of System F. In: Proceedings of eighth ACM SIGPLAN conference of functional programming, pp. 27–38 (2003)
Girard, J.-Y.: Interprétation functionelle et elimination des coupures de l’arithmètique d’ordre supérieur. PhD thesis, Université Paris VII (1972)
Honda, K., Yoshida, N.: Game theoretic analysis of call-by-value computation. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256. Springer, Heidelberg (1997)
Hughes, D.J.D.: Hypergame Semantics: Full Completeness for System F. PhD thesis, University of Oxford (1999)
Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF: I, II and III. Information and Computation 163, 285–408 (2000)
Laird, J.: A categorical semantics of higher-order store. In: Proceedings of CTCS 2002. ENTCS, vol. 69. Elsevier, Amsterdam (2002)
Laird, J.: Game semantics for a polymorphic programming language. In: Proc. LICS 2010 (2010) (to appear)
Levy, P.B.: Call-By-Push-Value. In: Semantic Structures in Computation. Kluwer, Dordrecht (2004)
Levy, P.B., Lassen, S.: Typed normal form bisimulation for parametric polymorphism. In: Proceedings of LICS 2008, pp. 341–552. IEEE press, Los Alamitos (2008)
Longo, G., Milsted, K., Soloviev, S.: The genericity theorem and parametricity in the polymorphic λ-calculus. Theoretical Computer Science 121(1&2), 323–349 (1993)
Pitts, A.: Polymorphism is set-theoretic constructively. In: Pitt, D. (ed.) CTCS 1988. LNCS, vol. 283, Springer, Heidelberg (1988)
Power, J., Thielecke, H.: Environments in Freyd categories and κ-categories. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644. Springer, Heidelberg (1999)
Power, J., Robinson, E.: Premonoidal categories and notions of computation. Mathematical Structures in Computer Science (1997)
Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, Springer, Heidelberg (1974)
Sanjabi, S., Ong, C.-H.L.: Fully abstract semantics of additive aspects by translation. In: Proceedings of Sixth International ACM Conference on Aspect-Oriented Software Development, pp. 135–148 (2007)
Seely, R.A.G.: Categorical semantics for higher-order polymorphic lambda-calculus. Journal of Symbolic Logic 52(4), 969–989 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laird, J. (2010). Game Semantics for Call-by-Value Polymorphism. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds) Automata, Languages and Programming. ICALP 2010. Lecture Notes in Computer Science, vol 6199. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14162-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-14162-1_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14161-4
Online ISBN: 978-3-642-14162-1
eBook Packages: Computer ScienceComputer Science (R0)