{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:54Z","timestamp":1776316914328,"version":"3.50.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171261","type":"print"},{"value":"9783030171278","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present a sound and complete bisimilarity for an untyped <jats:inline-formula>\n              <jats:tex-math>$$\\lambda $$<\/jats:tex-math>\n            <\/jats:inline-formula>-calculus with higher-order local references. Our relation compares values by applying them to a fresh variable, like normal-form bisimilarity, and it uses environments to account for the evolving store. We achieve completeness by a careful treatment of evaluation contexts comprising open stuck terms. This work improves over St\u00f8vring and Lassen\u2019s incomplete environment-based normal-form bisimilarity for the <jats:inline-formula>\n              <jats:tex-math>$$\\lambda \\rho $$<\/jats:tex-math>\n            <\/jats:inline-formula>-calculus, and confirms, in relatively elementary terms, Jaber and Tabareau\u2019s result, that the state construct is discriminative enough to be characterized with a bisimilarity without any quantification over testing arguments.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_6","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"98-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["A Complete Normal-Form Bisimilarity for State"],"prefix":"10.1007","author":[{"given":"Dariusz","family":"Biernacki","sequence":"first","affiliation":[]},{"given":"Sergue\u00ef","family":"Lenglet","sequence":"additional","affiliation":[]},{"given":"Piotr","family":"Polesiuk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Pierce, B.C. (ed.) Proceedings of the Thirty-Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 340\u2013353. ACM Press, January 2009","DOI":"10.1145\/1480881.1480925"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Aristiz\u00e1bal, A., Biernacki, D., Lenglet, S., Polesiuk, P.: Environmental bisimulations for delimited-control operators with dynamic prompt generation. Logical Methods Comput. Sci. 13(3) 2017","DOI":"10.23638\/LMCS-13(3:27)2017"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Lenglet, S., Polesiuk, P.: Proving soundness of extensional normal-form bisimilarities. In: Silva, A. (ed.) Proceedings of the 33rd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXXIII), Ljubljana, Slovenia. Electronic Notes in Theoretical Computer Science, vol. 336, pp. 41\u201356, June 2017","DOI":"10.1016\/j.entcs.2018.03.015"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normal-form bisimilarity for state. Research report RR-9251, Inria, Nancy, France, January 2019","DOI":"10.1007\/978-3-030-17127-8_6"},{"issue":"4\u20135","key":"6_CR5","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1017\/S095679681200024X","volume":"22","author":"D Dreyer","year":"2012","unstructured":"Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22(4\u20135), 477\u2013528 (2012)","journal-title":"J. Funct. Program."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-26529-2_15","volume-title":"Programming Languages and Systems","author":"G Jaber","year":"2015","unstructured":"Jaber, G., Tabareau, N.: Kripke open bisimulation \u2013 a marriage of game semantics and operational techniques. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 271\u2013291. Springer, Cham (2015)"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-02059-9_3","volume":"5","author":"R Jagadeesan","year":"2009","unstructured":"Jagadeesan, R., Pitcher, C., Riely, J.: Open bisimulation for aspects. Trans. Aspect-Oriented Softw. Dev. 5, 72\u2013132 (2009)","journal-title":"Trans. Aspect-Oriented Softw. Dev."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Koutavas, V., Levy, P.B., Sumii, E.: From applicative to environmental bisimulation. In: Mislove, M., Ouaknine, J. (eds.) Proceedings of the 27th Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXVII), Pittsburgh, PA, USA. ENTCS, vol. 276, pp. 215\u2013235, May 2011","DOI":"10.1016\/j.entcs.2011.09.023"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Morrisett, J.G., Jones, S.L.P. (eds.) POPL 2006, Charleston, SC, USA, pp. 141\u2013152. ACM Press (2006)","DOI":"10.1145\/1111037.1111050"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/978-3-540-73420-8_58","volume-title":"Automata, Languages and Programming","author":"J Laird","year":"2007","unstructured":"Laird, J.: A fully abstract trace semantics for general references. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 667\u2013679. Springer, Heidelberg (2007)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Lassen, S.B.: Eager normal form bisimulation. In: Panangaden, P. (ed.) LICS 2005, Chicago, IL, pp. 345\u2013354. IEEE Computer Society Press (2005)","DOI":"10.1109\/LICS.2005.15"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-662-44584-6_8","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"J-M Madiot","year":"2014","unstructured":"Madiot, J.-M., Pous, D., Sangiorgi, D.: Bisimulations up-to: beyond first-order transition systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 93\u2013108. Springer, Heidelberg (2014)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Murawski, A.S., Tzevelekos, N.: Game semantics for good general references. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pp. 75\u201384. IEEE Computer Society, June 2011","DOI":"10.1109\/LICS.2011.31"},{"issue":"3","key":"6_CR14","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10703-017-0292-9","volume":"52","author":"AS Murawski","year":"2018","unstructured":"Murawski, A.S., Tzevelekos, N.: Algorithmic games for full ground references. Formal Methods Syst. Des. 52(3), 277\u2013314 (2018)","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR15","unstructured":"Pitts, A., Stark, I.: Operational reasoning for functions with local state. In: Gordon, A., Pitts, A. (eds.) Higher Order Operational Techniques in Semantics, pp. 227\u2013273. Publications of the Newton Institute, Cambridge University Press (1998)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. In: Scedrov, A. (ed.) LICS 1992, Santa Cruz, California, pp. 102\u2013109. IEEE Computer Society (1992)","DOI":"10.1109\/LICS.1992.185524"},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1889997.1890002","volume":"33","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33(1), 1\u201369 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"St\u00f8vring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: Felleisen, M. (ed.) SIGPLAN Notices, POPL 2007, Nice, France, vol. 42, no. 1, pp. 161\u2013172. ACM Press (2007)","DOI":"10.1145\/1190215.1190244"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-04027-6_33","volume-title":"Computer Science Logic","author":"E Sumii","year":"2009","unstructured":"Sumii, E.: A complete characterization of observational equivalence in polymorphic $$\\lambda $$-calculus with general references. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 455\u2013469. Springer, Heidelberg (2009)"}],"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-030-17127-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T16:06:28Z","timestamp":1757088388000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}