Abstract
We present a formal correspondence between Laird’s trace semantics and the nominal game model of Murawski and Tzevelekos for RefML, a callby-value language with higher-order references. This gives an operational flavor to game semantics, where denotation of terms is generated via an interactive reduction, which allows to reduce terms with free functional variables, and where pointer structure is represented with name pointers. It also leads to transferring the categorical structure defined on the game model to the trace model. Then, representing the notion of view from game semantics in terms of available name pointers, we restrict our trace semantics to GroundML, a language with firstorder references and show its full abstraction using a correspondence with visible strategies. This gives the first fully abstract trace model for this language.
Chapter PDF
References
Abramsky, S., Ghica, D., Murawski, A., Ong, L., Stark, I.: Nominal games and full abstraction for the nu-calculus. In: Proceedings of LICS 2004, pp. 150–159. IEEE (2004)
Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: Proceedings of LICS 1998, pp. 334–344. IEEE (1998)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163(2), 409–470 (2000)
Gabbay, M., Ghica, D.: Game semantics in the nominal model. In: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012). Electronic Notes in Theoretical Computer Science, vol. 286, pp. 173–189. Elsevier (2012)
Gabbay, M., Pitts, A.: A new approach to abstract syntax with variable binding. Formal Aspects of computing 13(3-5), 341–363 (2002)
Hyland, M., Ong, L.: On full abstraction for PCF: I, II and III. Information and Computation 163(2), 285–408 (2000)
Jaber, G.: A Logical Study of Program Equivalence. PhD thesis, École des Mines de Nantes (2014)
Laird, J.: A game semantics of the asynchronous p-calculus. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 51–65. Springer, Heidelberg (2005)
Laird, J.: A fully abstract trace semantics for general references. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 667–679. Springer, Heidelberg (2007)
Laird, J.: A game semantics of names and pointers. Annals of Pure and Applied Logic 151(2), 151–169 (2008)
Laird, J.: Game semantics for call-by-value polymorphism. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 187–198. Springer, Heidelberg (2010)
Levy, P., Staton, S.: Transition systems over games. In: Proceedings of LICS 2014, pp. 64:1–64:10 (2014)
Murawski, A., Tzevelekos, N.: Game semantics for good general references. In: Proceedings of LICS 2011, pp. 75–84. IEEE (2011)
Murawski, A., Tzevelekos, N.: Algorithmic games for full ground references. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 312–324. Springer, Heidelberg (2012)
Murawski, A., Tzevelekos, N.: Full abstraction for reduced ml. Annals of Pure and Applied Logic (2013)
Power, J., Thielecke, H.: Closed freyd- and κ-categories. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 625–634. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jaber, G. (2015). Operational Nominal Game Semantics. In: Pitts, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2015. Lecture Notes in Computer Science(), vol 9034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46678-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-662-46678-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46677-3
Online ISBN: 978-3-662-46678-0
eBook Packages: Computer ScienceComputer Science (R0)