{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:10:27Z","timestamp":1765667427747,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308284"},{"type":"electronic","value":"9783031308291"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T00:00:00Z","timestamp":1682035200000},"content-version":"vor","delay-in-days":110,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove decidability for contextual equivalence of the<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu \\nu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>\u03bc<\/mml:mi><mml:mi>\u03bd<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus, that is the simply-typed call-by-value<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>\u03bc<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus equipped with booleans and fresh name creation, with contexts taken in<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu _{\\texttt{ref}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:msub><mml:mi>\u03bc<\/mml:mi><mml:mi>ref<\/mml:mi><\/mml:msub><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, that is<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu \\nu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>\u03bc<\/mml:mi><mml:mi>\u03bd<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus extended with higher-order references.<\/jats:p><jats:p>The proof exploits a labelled transition system capturing the interactions between<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu \\nu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>\u03bc<\/mml:mi><mml:mi>\u03bd<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>programs and<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda \\mu _{\\texttt{ref}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:msub><mml:mi>\u03bc<\/mml:mi><mml:mi>ref<\/mml:mi><\/mml:msub><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>contexts. The induced bisimulation equivalence is characterized as equality of certain trees, inspired by the work of Lassen. Since these trees are computable and finite, decidability follows. Bisimulation coincides also with trace equivalence, which in turn coincides with contextual equivalence.<\/jats:p>","DOI":"10.1007\/978-3-031-30829-1_2","type":"book-chapter","created":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:56:19Z","timestamp":1682020579000},"page":"24-45","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Deciding Contextual Equivalence of $$\\nu $$-Calculus with Effectful Contexts"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Hirschkoff","sequence":"first","affiliation":[]},{"given":"Guilhem","family":"Jaber","sequence":"additional","affiliation":[]},{"given":"Enguerrand","family":"Prebet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,21]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Samson Abramsky, Dan\u00a0R. Ghica, Andrzej\u00a0S. Murawski, C.-H.\u00a0Luke Ong, and Ian David\u00a0Bede Stark. Nominal games and full abstraction for the nu-calculus. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 150\u2013159. IEEE Computer Society, 2004.","DOI":"10.1109\/LICS.2004.1319609"},{"key":"2_CR2","unstructured":"Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998, pages 334\u2013344. IEEE Computer Society, 1998."},{"key":"2_CR3","unstructured":"Hendrik\u00a0Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985."},{"key":"2_CR4","unstructured":"Nick Benton, Martin Hofmann, and Vivek Nigam. Proof-relevant logical relations for name generation. Log. Methods Comput. Sci., 14(1), 2018."},{"key":"2_CR5","unstructured":"Nick Benton and Vasileios Koutavas. A mechanized bisimulation for the nu-calculus. Higher Order and Symbolic Computation - Special Issue in Honor of Mitchell Wand, sep 2012. In Press."},{"key":"2_CR6","unstructured":"Corrado B\u00f6hm. Alcune proprieta delle forme $$\\beta $$-$$\\eta $$-normali nel $$\\lambda $$-k-calcolo. Pubblicazioni dell\u2019Istituto per le Applicazioni del Calcolo, 696:19, 1968."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Murdoch Gabbay and Andrew\u00a0M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects Comput., 13(3-5):341\u2013363, 2002.","DOI":"10.1007\/s001650200016"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1\u2013102, 1987.","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"2_CR9","unstructured":"Daniel Hirschkoff, Guilhem Jaber, and Enguerrand Prebet. Deciding contextual equivalence of $$\\nu $$-calculus with effectful contexts (full version). https:\/\/hal.science\/hal-03955303."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Guilhem Jaber and Andrzej\u00a0S. Murawski. Complete trace models of state and control. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 348\u2013374. Springer, 2021.","DOI":"10.1007\/978-3-030-72019-3_13"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Guilhem Jaber and Andrzej\u00a0S. Murawski. Compositional relational reasoning via operational game semantics. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1\u201313. IEEE, 2021.","DOI":"10.1109\/LICS52264.2021.9470524"},{"key":"2_CR12","unstructured":"Guilhem Jaber and Davide Sangiorgi. Games, mobile processes, and functions. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, G\u00f6ttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 25:1\u201325:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022."},{"key":"2_CR13","unstructured":"James Laird. A fully abstract trace semantics for general references. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings, volume 4596 of Lecture Notes in Computer Science, pages 667\u2013679. Springer, 2007."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"James Laird. Sequentiality and the CPS semantics of fresh names. In Marcelo Fiore, editor, Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS 2007, New Orleans, LA, USA, April 11-14, 2007, volume 173 of Electronic Notes in Theoretical Computer Science, pages 203\u2013219. Elsevier, 2007.","DOI":"10.1016\/j.entcs.2007.02.035"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"James Laird. A Curry-style semantics of interaction: From untyped to second-order lazy $$\\lambda $$$$\\mu $$-calculus. In Jean Goubault-Larrecq and Barbara K\u00f6nig, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 422\u2013441. Springer, 2020.","DOI":"10.1007\/978-3-030-45231-5_22"},{"key":"2_CR16","unstructured":"S\u00f8ren\u00a0B. Lassen. Eager normal form bisimulation. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 345\u2013354. IEEE Computer Society, 2005."},{"key":"2_CR17","unstructured":"S\u00f8ren\u00a0B. Lassen and Paul\u00a0Blain Levy. Typed normal form bisimulation. In Jacques Duparc and Thomas\u00a0A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 283\u2013297. Springer, 2007."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Sam Lindley and Ian Stark. Reducibility and tt-lifting for computation types. In Pawel Urzyczyn, editor, Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 262\u2013277. Springer, 2005.","DOI":"10.1007\/11417170_20"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Andrzej\u00a0S. Murawski and Nikos Tzevelekos. Algorithmic nominal game semantics. In Gilles Barthe, editor, Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings, volume 6602 of Lecture Notes in Computer Science, pages 419\u2013438. Springer, 2011.","DOI":"10.1007\/978-3-642-19718-5_22"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Andrzej\u00a0S. Murawski and Nikos Tzevelekos. Full abstraction for reduced ML. Ann. Pure Appl. Log., 164(11):1118\u20131143, 2013.","DOI":"10.1016\/j.apal.2013.05.007"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Andrzej\u00a0S. Murawski and Nikos Tzevelekos. Algorithmic games for full ground references. Formal Methods Syst. Des., 52(3):277\u2013314, 2018.","DOI":"10.1007\/s10703-017-0292-9"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Michel Parigot. Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning,International Conference LPAR\u201992, St. Petersburg, Russia, July 15-20, 1992, Proceedings, volume 624 of Lecture Notes in Computer Science, pages 190\u2013201. Springer, 1992.","DOI":"10.1007\/BFb0013061"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Michel Parigot. Strong normalization for second order classical natural deduction. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS \u201993), Montreal, Canada, June 19-23, 1993, pages 39\u201346. IEEE Computer Society, 1993.","DOI":"10.1109\/LICS.1993.287602"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Andrew\u00a0M. Pitts and Ian David\u00a0Bede Stark. Observable properties of higher order functions that dynamically create local names, or what\u2019s new? In Andrzej\u00a0M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS\u201993, Gdansk, Poland, August 30 - September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 122\u2013141. Springer, 1993.","DOI":"10.1007\/3-540-57182-5_8"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"D.\u00a0Pous and D.\u00a0Sangiorgi. Advanced Topics in Bisimulation and Coinduction (D. Sangiorgi and J. Rutten editors), chapter Enhancements of the coinductive proof method. Cambridge University Press, 2011.","DOI":"10.1017\/CBO9780511792588"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman. Probabilistic programming semantics for name generation. Proc. ACM Program. Lang., 5(POPL):1\u201329, 2021.","DOI":"10.1145\/3434292"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447\u2013479, 1998.","DOI":"10.1017\/S0960129598002527"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Mark\u00a0R. Shinwell and Andrew\u00a0M. Pitts. On a monadic semantics for freshness. Theor. Comput. Sci., 342(1):28\u201355, 2005.","DOI":"10.1016\/j.tcs.2005.06.003"},{"key":"2_CR29","unstructured":"Ian Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, December 1994. Also available as Technical Report\u00a0363, University of Cambridge Computer Laboratory."},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Ian Stark. Categorical models for local names. LISP Symb. Comput., 9(1):77\u2013107, 1996.","DOI":"10.1007\/BF01806033"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Kristian St\u00f8vring and S\u00f8ren\u00a0B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In Jens Palsberg, editor, Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, volume 5700 of Lecture Notes in Computer Science, pages 329\u2013375. Springer, 2009.","DOI":"10.1007\/978-3-642-04164-8_17"},{"key":"2_CR32","unstructured":"Nikos Tzevelekos. Nominal Game Semantics. PhD thesis, University of Oxford, 2009."},{"key":"2_CR33","unstructured":"Nikos Tzevelekos. Program equivalence with names. In Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann, editors, Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, volume 10351 of Dagstuhl Seminar Proceedings. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany, 2010."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30829-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T22:42:38Z","timestamp":1729291358000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30829-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308284","9783031308291"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30829-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}