Abstract
We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either \(\mathrm {call/cc}\) or no control operator.
Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-order references and \(\mathrm {call/cc}\), constructed in the spirit of operational game semantics. Next we examine the impact of suppressing higher-order references and callcc in contexts and provide an operational explanation for the game-semantic conditions known as visibility and bracketing respectively. This allows us to refine the original model to provide fully abstract trace models of interaction with contexts that need not use higher-order references or \(\mathrm {call/cc}\). Along the way, we discuss the relationship between error- and termination-based contextual testing in each case, and relate the two to trace and complete trace equivalence respectively.
Overall, the paper provides a systematic development of operational game semantics for all four cases, which represent the state-based face of the so-called semantic cube.
The full version is available at https://hal.archives-ouvertes.fr/hal-03116698.
Chapter PDF
Similar content being viewed by others
References
Abramsky, S.: Games in the semantics of programming languages. In: Proceedings of the 11th Amsterdam Colloquium. pp. 1–6. ILLC, Dept. of Philosophy, University of Amsterdam (1997)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163, 409–470 (2000)
Abramsky, S., McCusker, G.: Call-by-value games. In: Proceedings of CSL. Lecture Notes in Computer Science, vol. 1414, pp. 1–17. Springer-Verlag (1997)
Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of POPL. pp. 340–353. ACM (2009)
Aristizabal, A., Biernacki, D., Lenglet, S., Polesiuk, P.: Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. Logical Methods in Computer Science 13(3) (2017)
Biernacki, D., Lenglet, S.: Environmental bisimulations for delimited-control operators. In: Proceedings of APLAS. Lecture Notes in Computer Science, vol. 8301, pp. 333–348. Springer (2013)
Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normal-form bisimilarity for state. In: Proceedings of FOSSACS. Lecture Notes in Computer Science, vol. 11425, pp. 98–114. Springer (2019)
Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22(4-5), 477–528 (2012)
Ghica, D.R., Tzevelekos, N.: A system-level game semantics. Electr. Notes Theor. Comput. Sci. 286, 191–211 (2012)
Honsell, F., Mason, I.A., Smith, S.F., Talcott, C.L.: A variable typed logic of effects. Inf. Comput. 119(1), 55–90 (1995)
Hur, C.K., Dreyer, D., Neis, G., Vafeiadis, V.: The marriage of bisimulations and kripke logical relations. In: Proceedings of POPL. pp. 59–72. ACM (2012)
Hyland, J.M.E., Ong, C.H.L.: On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Information and Computation 163(2), 285–408 (2000)
Jaber, G.: Operational nominal game semantics. In: Proceedings of FOSSACS. Lecture Notes in Computer Science, vol. 9034, pp. 264–278 (2015)
Jaber, G., Tabareau, N.: Kripke open bisimulation - A marriage of game semantics and operational techniques. In: Proceedings of APLAS. Lecture Notes in Computer Science, vol. 9458, pp. 271–291 (2015)
Jaber, G., Tzevelekos, N.: Trace semantics for polymorphic references. In: Proceedings of LICS. pp. 585–594. ACM (2016)
Jagadeesan, R., Pitcher, C., Riely, J.: Open bisimulation for aspects. In: Proceedings of AOSD. ACM International Conference Proceeding Series, vol. 208, pp. 107–120 (2007)
Jeffrey, A., Rathke, J.: Towards a theory of bisimulation for local names. In: Proceedings of LICS. pp. 56–66 (1999)
Jeffrey, A., Rathke, J.: A fully abstract may testing semantics for concurrent objects. Theor. Comput. Sci. 338(1-3), 17–63 (2005)
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Proceedings of POPL. pp. 141–152. ACM (2006)
Lago, U.D., Gavazzo, F.: Effectful normal form bisimulation. In: Proceedings of ESOP. Lecture Notes in Computer Science, vol. 11423, pp. 263–292. Springer (2019)
Lago, U.D., Gavazzo, F., Levy, P.B.: Effectful applicative bisimilarity: Monads, relators, and howe’s method. In: Proceedings of LICS. IEEE Press (2017)
Laird, J.: Full abstraction for functional languages with control. In: Proceedings of 12th IEEE Symposium on Logic in Computer Science. pp. 58–67 (1997)
Laird, J.: A fully abstract trace semantics for general references. In: Proceedings of ICALP, Lecture Notes in Computer Science, vol. 4596, pp. 667–679. Springer (2007)
Lassen, S.B., Levy, P.B.: Typed normal form bisimulation. In: Proceedings of CSL, Lecture Notes in Computer Science, vol. 4646, pp. 283–297. Springer (2007)
Levy, P.B., Staton, S.: Transition systems over games. In: Proceedings of CSL-LICS. pp. 64:1–64:10 (2014)
Milner, R.: Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4(1), 1–22 (1977)
Murawski, A.S., Tzevelekos, N.: Game semantics for good general references. In: Proceedings of LICS. pp. 75–84. IEEE Computer Society Press (2011)
Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher-Order Operational Techniques in Semantics, pp. 227–273. Cambridge University Press (1998)
Sangiorgi, D.: Expressing mobility in process algebras: First-order and higher-order paradigms. Tech. Rep. CST-99-93, University of Edinburgh (1993), PhD thesis
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33(1), 5 (2011)
Støvring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: POPL. pp. 161–172. ACM (2007)
Sumii, E.: A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. In: Proceedings of CSL. Lecture Notes in Computer Science, vol. 5771, pp. 455–469. Springer (2009)
Talcott, C.L.: Reasoning about functions with effects. In: Gordon, A.D., Pitts, A.M. (eds.) Higher-Order Operational Techniques in Semantics, pp. 347–390. Cambridge University Press (1998)
Yachi, T., Sumii, E.: A sound and complete bisimulation for contextual equivalence in \(\lambda \)-calculus with call/cc. In: Proceedings of APLAS. pp. 171–186. Springer (2016)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Jaber, G., Murawski, A.S. (2021). Complete trace models of state and control. In: Yoshida, N. (eds) Programming Languages and Systems. ESOP 2021. Lecture Notes in Computer Science(), vol 12648. Springer, Cham. https://doi.org/10.1007/978-3-030-72019-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-72019-3_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72018-6
Online ISBN: 978-3-030-72019-3
eBook Packages: Computer ScienceComputer Science (R0)