{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T13:32:20Z","timestamp":1764250340513,"version":"3.46.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"6","funder":[{"name":"Science Foundation Ireland","award":["13\/RC\/2094_2"],"award-info":[{"award-number":["13\/RC\/2094_2"]}]},{"name":"Irish Research Council","award":["GOIPD\/2024\/809"],"award-info":[{"award-number":["GOIPD\/2024\/809"]}]},{"name":"Cisco University Research Program Fund, a corporate advised fund of Silicon Valley Community Foundation; and Ethereum Foundation","award":["FY23-1127"],"award-info":[{"award-number":["FY23-1127"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>\n                    We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF\n                    <jats:sub>v<\/jats:sub>\n                    ). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and game semantics. In order to obtain completeness while avoiding the use of semantic quotienting, the LTS constructs traces corresponding to interactions with possible functional contexts. The model gives rise to a sound and complete technique for checking of PCF\n                    <jats:sub>v<\/jats:sub>\n                    program equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples.\n                  <\/jats:p>","DOI":"10.1145\/3765737","type":"journal-article","created":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T11:19:47Z","timestamp":1758021587000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Fully Abstract Normal Form Bisimulation for Call-by-Value PCF"],"prefix":"10.1145","volume":"72","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3970-2486","authenticated-orcid":false,"given":"Vasileios","family":"Koutavas","sequence":"first","affiliation":[{"name":"Trinity College Dublin","place":["Dublin, Ireland"]},{"name":"Lero - Science Foundation Ireland Research Centre for Software","place":["Dublin, Ireland"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5783-9454","authenticated-orcid":false,"given":"Yu-Yang","family":"Lin","sequence":"additional","affiliation":[{"name":"Trinity College Dublin","place":["Dublin, Ireland"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8509-8059","authenticated-orcid":false,"given":"Nikos","family":"Tzevelekos","sequence":"additional","affiliation":[{"name":"Queen Mary University of London","place":["London, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,11,27]]},"reference":[{"key":"e_1_3_4_2_2","volume-title":"Research Topics in Functional Programming","author":"Abramsky Samson","year":"1990","unstructured":"Samson Abramsky. 1990. The lazy lambda calculus. Research Topics in Functional Programming. Addison-Wesley Longman Publishing Co., Inc."},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_3_4_4_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0028004","volume-title":"Proceedings of the Computer Science Logic, 11th International Workshop","volume":"1414","author":"Abramsky Samson","year":"1998","unstructured":"Samson Abramsky and Guy McCusker. 1998. Call-by-value games. In Proceedings of the Computer Science Logic, 11th International Workshop(LNCS, Vol. 1414). Mogens Nielsen and Wolfgang Thomas (Eds.), Springer, Berlin, 1\u201317. DOI:10.1007\/BFB0028004"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_4_6_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/978-3-642-29822-6_7","volume-title":"Proceedings of the Functional and Logic Programming\u201411th International Symposium.","volume":"7294","author":"Biernacki Dariusz","year":"2012","unstructured":"Dariusz Biernacki and Sergue\u00ef Lenglet. 2012. Normal form bisimulations for delimited-control operators. In Proceedings of the Functional and Logic Programming\u201411th International Symposium.Tom Schrijvers and Peter Thiemann (Eds.), Lecture Notes in Computer Science, Vol. 7294, Springer, Berlin,47\u201361. DOI:10.1007\/978-3-642-29822-6_7"},{"key":"e_1_3_4_7_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-030-17127-8_6","volume-title":"Proceedings of the Foundations of Software Science and Computation Structures - 22nd International Conference.","volume":"11425","author":"Biernacki Dariusz","year":"2019","unstructured":"Dariusz Biernacki, Sergue\u00ef Lenglet, and Piotr Polesiuk. 2019. A complete normal-form bisimilarity for state. In Proceedings of the Foundations of Software Science and Computation Structures - 22nd International Conference.Mikolaj Bojanczyk and Alex Simpson (Eds.), Lecture Notes in Computer Science, Vol. 11425, Springer International Publishing, Cham, 98\u2013114. DOI:10.1007\/978-3-030-17127-8_6"},{"key":"e_1_3_4_8_2","unstructured":"Martin Churchill James Laird and Guy McCusker. 2010. A Concrete Representation of Observational Equivalence for PCF. arXiv:1003.0107. Retrieved from https:\/\/arxiv.org\/abs\/1003.0107"},{"key":"e_1_3_4_9_2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"191","volume-title":"Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics.","volume":"286","author":"Ghica Dan R.","year":"2012","unstructured":"Dan R. Ghica and Nikos Tzevelekos. 2012. A system-level game semantics. In Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics.Ulrich Berger and Michael W. Mislove (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 286, Elsevier, 191\u2013211. DOI:10.1016\/j.entcs.2012.08.013"},{"key":"e_1_3_4_10_2","volume-title":"Functional Programming and Input\/Output","author":"Gordon Andrew Donald","year":"1992","unstructured":"Andrew Donald Gordon. 1992. Functional Programming and Input\/Output. Ph. D. Dissertation. University of Cambridge, UK."},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00039-0"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1996.0008"},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_3_4_14_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/978-3-662-46678-0_17","volume-title":"Proceedings of the Foundations of Software Science and Computation Structures\u201418th International Conference, FoSSaCS 2015.","volume":"9034","author":"Jaber Guilhem","year":"2015","unstructured":"Guilhem Jaber. 2015. Operational nominal game semantics. In Proceedings of the Foundations of Software Science and Computation Structures\u201418th International Conference, FoSSaCS 2015.Andrew M. Pitts (Ed.), Lecture Notes in Computer Science, Vol. 9034, Springer, Berlin,264\u2013278. DOI:10.1007\/978-3-662-46678-0_17"},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02059-9_3"},{"key":"e_1_3_4_16_2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"215","volume-title":"Proceedings of the 27th Conference on the Mathematical Foundations of Programming Semantics.","volume":"276","author":"Koutavas Vasileios","year":"2011","unstructured":"Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. 2011. From applicative to environmental bisimulation. In Proceedings of the 27th Conference on the Mathematical Foundations of Programming Semantics.Michael W. Mislove and Jo\u00ebl Ouaknine (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 276, Elsevier, 215\u2013235. DOI:10.1016\/J.ENTCS.2011.09.023"},{"key":"e_1_3_4_17_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-030-99527-0_10","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference.","volume":"13244","author":"Koutavas Vasileios","year":"2022","unstructured":"Vasileios Koutavas, Yu-Yang Lin, and Nikos Tzevelekos. 2022. From bounded checking to verification of equivalence via symbolic up-to techniques. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference.Dana Fisman and Grigore Rosu (Eds.), Lecture Notes in Computer Science, Vol. 13244, Springer International Publishing, Cham, 178\u2013195. DOI:10.1007\/978-3-030-99527-0_10"},{"key":"e_1_3_4_18_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/11693024_11","volume-title":"Proceedings of the Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006.","volume":"3924","author":"Koutavas Vasileios","year":"2006","unstructured":"Vasileios Koutavas and Mitchell Wand. 2006. Bisimulations for untyped imperative objects. In Proceedings of the Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006.Peter Sestoft (Ed.), Lecture Notes in Computer Science, Vol. 3924, Springer,Berlin, 146\u2013161. DOI:10.1007\/11693024_11"},{"key":"e_1_3_4_19_2","first-page":"141","volume-title":"Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Koutavas Vasileios","year":"2006","unstructured":"Vasileios Koutavas and Mitchell Wand. 2006. Small bisimulations for reasoning about higher-order imperative programs. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. J. Gregory Morrisett and Simon L. Peyton Jones (Eds.), ACM, Charleston South Carolina USA, 141\u2013152. DOI:10.1145\/1111037.1111050"},{"key":"e_1_3_4_20_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1007\/978-3-540-73420-8_58","volume-title":"Proceedings of the Automata, Languages and Programming, 34th International Colloquium.","volume":"4596","author":"Laird James","year":"2007","unstructured":"James Laird. 2007. A fully abstract trace semantics for general references. In Proceedings of the Automata, Languages and Programming, 34th International Colloquium.Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki (Eds.), Lecture Notes in Computer Science, Vol. 4596, Springer, Berlin, 667\u2013679. DOI:10.1007\/978-3-540-73420-8_58"},{"key":"e_1_3_4_21_2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"346","volume-title":"Proceedings of the 15th Conference on Mathematical Foundations of Progamming Semantics (MFPS XV).","volume":"20","author":"Lassen S\u00f8ren B.","year":"1999","unstructured":"S\u00f8ren B. Lassen. 1999. Bisimulation in untyped lambda calculus: B\u00f6hm trees and bisimulation up to context. In Proceedings of the 15th Conference on Mathematical Foundations of Progamming Semantics (MFPS XV).Stephen D. Brookes, Achim Jung, Michael W. Mislove, and Andre Scedrov (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 20, Elsevier BV, 346\u2013374. DOI:10.1016\/S1571-0661(04)80083-5"},{"key":"e_1_3_4_22_2","first-page":"345","volume-title":"Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA.","author":"Lassen S\u00f8ren B.","year":"2005","unstructured":"S\u00f8ren B. Lassen. 2005. Eager normal form bisimulation. In Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA.IEEE, Chicago, IL, USA, 345\u2013354. DOI:10.1109\/LICS.2005.15"},{"key":"e_1_3_4_23_2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"445","volume-title":"Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI).","volume":"155","author":"Lassen S\u00f8ren B.","year":"2006","unstructured":"S\u00f8ren B. Lassen. 2006. Normal form simulation for McCarthy\u2019s amb. In Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI).Mart\u00edn H\u00f6tzel Escard\u00f3, Achim Jung, and Michael W. Mislove (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 155, Elsevier, 445\u2013465. DOI:10.1016\/j.entcs.2005.11.068"},{"key":"e_1_3_4_24_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/978-3-540-74915-8_23","volume-title":"Proceedings of the Computer Science Logic, 21st International Workshop.","volume":"4646","author":"Lassen S\u00f8ren B.","year":"2007","unstructured":"S\u00f8ren B. Lassen and Paul Blain Levy. 2007. Typed normal form bisimulation. In Proceedings of the Computer Science Logic, 21st International Workshop.Jacques Duparc and Thomas A. Henzinger (Eds.), Lecture Notes in Computer Science, Vol. 4646, Springer, Berlin, 283\u2013297. DOI:10.1007\/978-3-540-74915-8_23"},{"key":"e_1_3_4_25_2","first-page":"341","volume-title":"Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science","author":"Lassen S\u00f8ren B.","year":"2008","unstructured":"S\u00f8ren B. Lassen and Paul Blain Levy. 2008. Typed normal form bisimulation for parametric polymorphism. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science. IEEE, Pittsburgh, PA, USA, 341\u2013352. DOI:10.1109\/LICS.2008.26"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00194-8"},{"key":"e_1_3_4_27_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0615-9","volume-title":"Games and Full Abstraction for a Functional Metalanguage with Recursive Types","author":"McCusker Guy","year":"1998","unstructured":"Guy McCusker. 1998. Games and Full Abstraction for a Functional Metalanguage with Recursive Types. Springer."},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"e_1_3_4_29_2","volume-title":"Lambda Calculus Models of Programming Languages","author":"Jr. J. H. Morris,","year":"1968","unstructured":"J. H. Morris, Jr.1968. Lambda Calculus Models of Programming Languages. Ph. D. Dissertation. MIT, Cambridge, MA."},{"key":"e_1_3_4_30_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-58140-5_25","volume-title":"Proceedings of the Logical Foundations of Computer Science, 3rd International Symposium, LFCS\u201994, St. Petersburg, Russia, July 11-14, 1994.","volume":"813","author":"Nickau Hanno","year":"1994","unstructured":"Hanno Nickau. 1994. Hereditarily sequential functionals. In Proceedings of the Logical Foundations of Computer Science, 3rd International Symposium, LFCS\u201994, St. Petersburg, Russia, July 11-14, 1994.Anil Nerode and Yuri V. Matiyasevich (Eds.), Lecture Notes in Computer Science, Vol. 813, Springer, Berlin, 253\u2013264. DOI:10.1007\/3-540-58140-5_25"},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1995.1103"},{"key":"e_1_3_4_32_2","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BFb0055063","volume-title":"Proceedings of the Automata, Languages and Programming","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts. 1998. Existential types: Logical relations and operational equivalence. In Proceedings of the Automata, Languages and Programming. Kim G. Larsen, Sven Skyum, and Glynn Winskel (Eds.), Springer, Berlin, 309\u2013326. DOI:10.1007\/BFB0055063"},{"key":"e_1_3_4_33_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_4_35_2","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1017\/CBO9780511792588.007","volume-title":"Proceedings of the Advanced Topics in Bisimulation and Coinduction","volume":"52","author":"Pous Damien","year":"2011","unstructured":"Damien Pous and Davide Sangiorgi. 2011. Enhancements of the bisimulation proof method. In Proceedings of the Advanced Topics in Bisimulation and Coinduction. Davide Sangiorgi and Jan J. M. M. Rutten (Eds.), Cambridge Tracts in Theoretical Computer Science, Vol. 52. Cambridge University Press, 233\u2013289. DOI:10.1017\/CBO9780511792588.007"},{"key":"e_1_3_4_36_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1042"},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890002"},{"key":"e_1_3_4_38_2","first-page":"161","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"St\u00f8vring Kristian","year":"2007","unstructured":"Kristian St\u00f8vring and S\u00f8ren B. Lassen. 2007. A complete, co-inductive syntactic theory of sequential control and state. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Martin Hofmann and Matthias Felleisen (Eds.), ACM, Nice France, 161\u2013172. DOI:10.1145\/1190216.1190244"},{"key":"e_1_3_4_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.032"},{"key":"e_1_3_4_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1284320.1284325"},{"key":"e_1_3_4_41_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(3:8)2009"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3765737","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T13:28:42Z","timestamp":1764250122000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3765737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,27]]},"references-count":40,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3765737"],"URL":"https:\/\/doi.org\/10.1145\/3765737","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2025,11,27]]},"assertion":[{"value":"2023-11-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-07-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}