{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:44Z","timestamp":1780994684048,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T00:00:00Z","timestamp":1663632000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,9,20]]},"DOI":"10.1145\/3551357.3551374","type":"proceedings-article","created":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T15:37:25Z","timestamp":1663688245000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Contextual Equivalence in a Probabilistic Call-by-Need Lambda-Calculus"],"prefix":"10.1145","author":[{"given":"David","family":"Sabel","sequence":"first","affiliation":[{"name":"LMU Munich, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"additional","affiliation":[{"name":"University Frankfurt am Main, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luca","family":"Maio","sequence":"additional","affiliation":[{"name":"LMU Munich, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"AProVE. 2022. Homepage of AProVE. http:\/\/aprove.informatik.rwth-aachen.de.  AProVE. 2022. Homepage of AProVE. http:\/\/aprove.informatik.rwth-aachen.de."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473592"},{"key":"e_1_3_2_1_5_1","volume-title":"FoSSaCS 2015(LNCS), Vol.\u00a09034","author":"Bizjak Ales","unstructured":"Ales Bizjak and Lars Birkedal . 2015. Step-Indexed Logical Relations for Probability . In FoSSaCS 2015(LNCS), Vol.\u00a09034 . Springer , 279\u2013294. https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18 10.1007\/978-3-662-46678-0_18 Ales Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In FoSSaCS 2015(LNCS), Vol.\u00a09034. Springer, 279\u2013294. https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18"},{"key":"e_1_3_2_1_6_1","unstructured":"CeTA. 2022. Homepage of CeTA. http:\/\/cl-informatik.uibk.ac.at\/software\/ceta.  CeTA. 2022. Homepage of CeTA. http:\/\/cl-informatik.uibk.ac.at\/software\/ceta."},{"key":"e_1_3_2_1_7_1","volume-title":"ESOP\u00a02014(LNCS), Vol.\u00a08410","author":"Crubill\u00e9 Raphaelle","unstructured":"Raphaelle Crubill\u00e9 and Ugo Dal Lago . 2014. On Probabilistic Applicative Bisimulation and Call-by-Value \u03bb-Calculi . In ESOP\u00a02014(LNCS), Vol.\u00a08410 . Springer , 209\u2013228. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_12 10.1007\/978-3-642-54833-8_12 Raphaelle Crubill\u00e9 and Ugo Dal Lago. 2014. On Probabilistic Applicative Bisimulation and Call-by-Value \u03bb-Calculi. In ESOP\u00a02014(LNCS), Vol.\u00a08410. Springer, 209\u2013228. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_12"},{"key":"#cr-split#-e_1_3_2_1_8_1.1","doi-asserted-by":"crossref","unstructured":"Ugo Dal Lago. 2020. On Probabilistic \u039b-Calculi. Cambridge University Press 121-144. https:\/\/doi.org\/10.1017\/9781108770750.005 10.1017\/9781108770750.005","DOI":"10.1017\/9781108770750.005"},{"key":"#cr-split#-e_1_3_2_1_8_1.2","doi-asserted-by":"crossref","unstructured":"Ugo Dal Lago. 2020. On Probabilistic \u039b-Calculi. Cambridge University Press 121-144. https:\/\/doi.org\/10.1017\/9781108770750.005","DOI":"10.1017\/9781108770750.005"},{"key":"e_1_3_2_1_9_1","volume-title":"Effectful Normal Form Bisimulation. In ESOP 2019(LNCS), Vol.\u00a011423","author":"Dal Lago U.","unstructured":"U. Dal Lago and F. Gavazzo . 2019 . Effectful Normal Form Bisimulation. In ESOP 2019(LNCS), Vol.\u00a011423 . Springer, 263\u2013292. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_10 10.1007\/978-3-030-17184-1_10 U. Dal Lago and F. Gavazzo. 2019. Effectful Normal Form Bisimulation. In ESOP 2019(LNCS), Vol.\u00a011423. Springer, 263\u2013292. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_10"},{"key":"e_1_3_2_1_10_1","volume-title":"FoSSaCS 2020(LNCS), Vol.\u00a012077","author":"Lago Ugo Dal","unstructured":"Ugo Dal Lago , Giulio Guerrieri , and Willem Heijltjes . 2020. Decomposing Probabilistic Lambda-Calculi . In FoSSaCS 2020(LNCS), Vol.\u00a012077 . Springer , 136\u2013156. https:\/\/doi.org\/10.1007\/978-3-030-45231-5_8 10.1007\/978-3-030-45231-5_8 Ugo Dal Lago, Giulio Guerrieri, and Willem Heijltjes. 2020. Decomposing Probabilistic Lambda-Calculi. In FoSSaCS 2020(LNCS), Vol.\u00a012077. Springer, 136\u2013156. https:\/\/doi.org\/10.1007\/978-3-030-45231-5_8"},{"key":"e_1_3_2_1_11_1","volume-title":"POPL","author":"Lago Ugo Dal","year":"2014","unstructured":"Ugo Dal Lago , Davide Sangiorgi , and Michele Alberti . 2014. On coinductive equivalences for higher-order probabilistic functional programs . In POPL 2014 . ACM , 297\u2013308. https:\/\/doi.org\/10.1145\/2535838.2535872 10.1145\/2535838.2535872 Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. 2014. On coinductive equivalences for higher-order probabilistic functional programs. In POPL 2014. ACM, 297\u2013308. https:\/\/doi.org\/10.1145\/2535838.2535872"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012012"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785699"},{"key":"e_1_3_2_1_14_1","volume-title":"Proving Termination of Programs Automatically with AProVE. In IJCAR 2014(LNCS), Vol.\u00a08562","author":"Giesl J\u00fcrgen","year":"2014","unstructured":"J\u00fcrgen Giesl , Marc Brockschmidt , Fabian Emmes , Florian Frohn , Carsten Fuhs , Carsten Otto , Martin Pl\u00fccker , Peter Schneider-Kamp , Thomas Str\u00f6der , Stephanie Swiderski , and Ren\u00e9 Thiemann . 2014 . Proving Termination of Programs Automatically with AProVE. In IJCAR 2014(LNCS), Vol.\u00a08562 . Springer, 184\u2013191. https:\/\/doi.org\/10.1007\/978-3-319-08587-6_13 10.1007\/978-3-319-08587-6_13 J\u00fcrgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Pl\u00fccker, Peter Schneider-Kamp, Thomas Str\u00f6der, Stephanie Swiderski, and Ren\u00e9 Thiemann. 2014. Proving Termination of Programs Automatically with AProVE. In IJCAR 2014(LNCS), Vol.\u00a08562. Springer, 184\u2013191. https:\/\/doi.org\/10.1007\/978-3-319-08587-6_13"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39173"},{"key":"e_1_3_2_1_16_1","volume-title":"RTA 2009(LNCS), Vol.\u00a05595","author":"Korp Martin","unstructured":"Martin Korp , Christian Sternagel , Harald Zankl , and Aart Middeldorp . 2009. Tyrolean Termination Tool 2 . In RTA 2009(LNCS), Vol.\u00a05595 . Springer , 295\u2013304. https:\/\/doi.org\/10.1007\/978-3-642-02348-4_21 10.1007\/978-3-642-02348-4_21 Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. 2009. Tyrolean Termination Tool 2. In RTA 2009(LNCS), Vol.\u00a05595. Springer, 295\u2013304. https:\/\/doi.org\/10.1007\/978-3-642-02348-4_21"},{"key":"#cr-split#-e_1_3_2_1_17_1.1","doi-asserted-by":"crossref","unstructured":"Arne Kutzner and Manfred Schmidt-Schau\u00df. 1998. A Non-Deterministic Call-by-Need Lambda Calculus. In ICFP\u00a01998. ACM 324-335. https:\/\/doi.org\/10.1145\/289423.289462 10.1145\/289423.289462","DOI":"10.1145\/291251.289462"},{"key":"#cr-split#-e_1_3_2_1_17_1.2","doi-asserted-by":"crossref","unstructured":"Arne Kutzner and Manfred Schmidt-Schau\u00df. 1998. A Non-Deterministic Call-by-Need Lambda Calculus. In ICFP\u00a01998. ACM 324-335. https:\/\/doi.org\/10.1145\/289423.289462","DOI":"10.1145\/291251.289462"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0061"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48919-3_8"},{"key":"e_1_3_2_1_20_1","first-page":"1","article-title":"Erratic Fudgets: a semantic theory for an embedded coordination language. Sci","volume":"46","author":"Moran Andrw","year":"2003","unstructured":"Andrw Moran , David Sands , and Magnus Carlsson . 2003 . Erratic Fudgets: a semantic theory for an embedded coordination language. Sci . Comput. Program. 46 , 1 - 2 (2003), 99\u2013135. https:\/\/doi.org\/10.1016\/S0167-6423(02)00088-6 10.1016\/S0167-6423(02)00088-6 Andrw Moran, David Sands, and Magnus Carlsson. 2003. Erratic Fudgets: a semantic theory for an embedded coordination language. Sci. Comput. Program. 46, 1-2 (2003), 99\u2013135. https:\/\/doi.org\/10.1016\/S0167-6423(02)00088-6","journal-title":"Comput. Program."},{"key":"e_1_3_2_1_22_1","volume-title":"FSTTCS\u00a01995(LNCS), Vol.\u00a01026","author":"Panangaden Prakash","unstructured":"Prakash Panangaden . 1995. The Expressive Power of Indeterminate Primitives in Asynchronous Computation . In FSTTCS\u00a01995(LNCS), Vol.\u00a01026 . Springer , 124\u2013150. https:\/\/doi.org\/10.1007\/3-540-60692-0 10.1007\/3-540-60692-0 Prakash Panangaden. 1995. The Expressive Power of Indeterminate Primitives in Asynchronous Computation. In FSTTCS\u00a01995(LNCS), Vol.\u00a01026. Springer, 124\u2013150. https:\/\/doi.org\/10.1007\/3-540-60692-0"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_36"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.289.2"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006774"},{"key":"e_1_3_2_1_26_1","volume-title":"A Probabilistic Call-by-Need Lambda-Calculus \u2013 Extended Version. CoRR","author":"Sabel David","year":"2022","unstructured":"David Sabel , Manfred Schmidt-Schau\u00df , and Luca Maio . 2022. A Probabilistic Call-by-Need Lambda-Calculus \u2013 Extended Version. CoRR ( 2022 ). https:\/\/doi.org\/10.48550\/ARXIV.2205.14916 10.48550\/ARXIV.2205.14916 David Sabel, Manfred Schmidt-Schau\u00df, and Luca Maio. 2022. A Probabilistic Call-by-Need Lambda-Calculus \u2013 Extended Version. CoRR (2022). https:\/\/doi.org\/10.48550\/ARXIV.2205.14916"},{"key":"e_1_3_2_1_27_1","volume-title":"Probabilistic LCF. In MFCS 1978(LNCS), Vol.\u00a064","author":"Saheb-Djahromi Nasser","year":"1978","unstructured":"Nasser Saheb-Djahromi . 1978 . Probabilistic LCF. In MFCS 1978(LNCS), Vol.\u00a064 . Springer, 442\u2013451. https:\/\/doi.org\/10.1007\/3-540-08921-7_92 10.1007\/3-540-08921-7_92 Nasser Saheb-Djahromi. 1978. Probabilistic LCF. In MFCS 1978(LNCS), Vol.\u00a064. Springer, 442\u2013451. https:\/\/doi.org\/10.1007\/3-540-08921-7_92"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3350618"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2010.01.001"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.12.001"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968603"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2011.04.011"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006624"},{"key":"e_1_3_2_1_34_1","volume-title":"TPHOLs 2009(LNCS), Vol.\u00a05674","author":"Thiemann Ren\u00e9","unstructured":"Ren\u00e9 Thiemann and Christian Sternagel . 2009. Certification of Termination Proofs Using CeTA . In TPHOLs 2009(LNCS), Vol.\u00a05674 . Springer , 452\u2013468. https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31 10.1007\/978-3-642-03359-9_31 Ren\u00e9 Thiemann and Christian Sternagel. 2009. Certification of Termination Proofs Using CeTA. In TPHOLs 2009(LNCS), Vol.\u00a05674. Springer, 452\u2013468. https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31"},{"key":"e_1_3_2_1_35_1","unstructured":"TTT2. 2022. Homepage of TTT2. http:\/\/cl-informatik.uibk.ac.at\/software\/ttt2\/.  TTT2. 2022. Homepage of TTT2. http:\/\/cl-informatik.uibk.ac.at\/software\/ttt2\/."}],"event":{"name":"PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming","location":"Tbilisi Georgia","acronym":"PPDP 2022"},"container-title":["Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551374","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551357.3551374","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:24Z","timestamp":1750186824000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551374"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,20]]},"references-count":36,"alternative-id":["10.1145\/3551357.3551374","10.1145\/3551357"],"URL":"https:\/\/doi.org\/10.1145\/3551357.3551374","relation":{},"subject":[],"published":{"date-parts":[[2022,9,20]]},"assertion":[{"value":"2022-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}