{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:57Z","timestamp":1776316917069,"version":"3.50.1"},"publisher-location":"Cham","reference-count":73,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171834","type":"print"},{"value":"9783030171841","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"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17184-1_10","type":"book-chapter","created":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T21:34:04Z","timestamp":1554586444000},"page":"263-292","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Effectful Normal Form Bisimulation"],"prefix":"10.1007","author":[{"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Gavazzo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,6]]},"reference":[{"key":"10_CR1","first-page":"65","volume-title":"Research Topics in Functional Programming","author":"S Abramsky","year":"1990","unstructured":"Abramsky, S.: The lazy lambda calculus. In: Turner, D. (ed.) Research Topics in Functional Programming, pp. 65\u2013117. Addison Wesley, Boston (1990)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Jung, A.: Domain theory. In: Handbook of Logic in Computer Science, pp. 1\u2013168. Clarendon Press (1994)","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"issue":"2","key":"10_CR3","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1006\/inco.1993.1044","volume":"105","author":"S Abramsky","year":"1993","unstructured":"Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159\u2013267 (1993)","journal-title":"Inf. Comput."},{"issue":"5","key":"10_CR4","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A Appel","year":"2001","unstructured":"Appel, A., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR5","unstructured":"Barendregt, H.: The lambda calculus: its syntax and semantics. In: Studies in Logic and the Foundations of Mathematics. North-Holland (1984)"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BFb0060439","volume":"137","author":"M Barr","year":"1970","unstructured":"Barr, M.: Relational algebras. Lect. Notes Math. 137, 39\u201355 (1970)","journal-title":"Lect. Notes Math."},{"issue":"1","key":"10_CR7","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1016\/j.jlamp.2014.02.001","volume":"84","author":"A Bauer","year":"2015","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84(1), 108\u2013123 (2015)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Benton, N., Kennedy, A., Beringer, L., Hofmann, M.: Relational semantics for effect-based program transformations: higher-order store. In: Proceedings of PPDP 2009, pp. 301\u2013312 (2009)","DOI":"10.1145\/1599410.1599447"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.entcs.2018.03.015","volume":"336","author":"D Biernacki","year":"2018","unstructured":"Biernacki, D., Lenglet, S., Polesiuk, P.: Proving soundness of extensional normal-form bisimilarities. Electr. Notes Theor. Comput. Sci. 336, 41\u201356 (2018)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-662-46678-0_18","volume-title":"Foundations of Software Science and Computation Structures","author":"A Bizjak","year":"2015","unstructured":"Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 279\u2013294. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18"},{"key":"10_CR11","unstructured":"B\u00f6hm, C.: Alcune propriet\u00e0 delle forme $$\\beta \\eta $$ -normali del $$\\lambda k$$ -calcolo. Pubblicazioni dell\u2019Istituto per le Applicazioni del Calcolo 696 (1968)"},{"key":"10_CR12","volume-title":"A Course in Universal Algebra. Graduate Texts in Mathematics","author":"S Burris","year":"1981","unstructured":"Burris, S., Sankappanavar, H.: A Course in Universal Algebra. Graduate Texts in Mathematics. Springer, New York (1981)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-54833-8_12","volume-title":"Programming Languages and Systems","author":"R Crubill\u00e9","year":"2014","unstructured":"Crubill\u00e9, R., Dal Lago, U.: On probabilistic applicative bisimulation and call-by-value $$\\lambda $$ -Calculi. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 209\u2013228. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_12"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-662-54434-1_14","volume-title":"Programming Languages and Systems","author":"R Culpepper","year":"2017","unstructured":"Culpepper, R., Cobb, A.: Contextual equivalence for probabilistic programs with continuous random variables and scoring. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 368\u2013392. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_14"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Gavazzo, F., Levy, P.: Effectful applicative bisimilarity: monads, relators, and Howe\u2019s method. In: Proceedings of LICS 2017, pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005117"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Sangiorgi, D., Alberti, M.: On coinductive equivalences for higher-order probabilistic functional programs. In: Proceedings of POPL 2014, pp. 297\u2013308 (2014)","DOI":"10.1145\/2535838.2535872"},{"issue":"3","key":"10_CR17","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1051\/ita\/2012012","volume":"46","author":"U Lago Dal","year":"2012","unstructured":"Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. Appl. 46(3), 413\u2013450 (2012)","journal-title":"RAIRO - Theor. Inf. Appl."},{"issue":"3","key":"10_CR18","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/507382.507385","volume":"3","author":"V Danos","year":"2002","unstructured":"Danos, V., Harmer, R.: Probabilistic game semantics. ACM Trans. Comput. Logic 3(3), 359\u2013382 (2002)","journal-title":"ACM Trans. Comput. Logic"},{"key":"10_CR19","volume-title":"Introduction to Lattices and Order","author":"B Davey","year":"1990","unstructured":"Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"issue":"2","key":"10_CR20","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1995.1145","volume":"122","author":"U Liguoro De","year":"1995","unstructured":"De Liguoro, U., Piperno, A.: Non deterministic extensions of untyped lambda-calculus. Inf. Comput. 122(2), 149\u2013177 (1995)","journal-title":"Inf. Comput."},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Durier, A., Hirschkoff, D., Sangiorgi, D.: Eager functions as processes. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, pp. 364\u2013373 (2018)","DOI":"10.1145\/3209108.3209152"},{"issue":"2","key":"10_CR22","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235\u2013271 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Gavazzo, F.: Quantitative behavioural reasoning for higher-order effectful programs: applicative distances. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09\u201312 July 2018, pp. 452\u2013461 (2018)","DOI":"10.1145\/3209108.3209149"},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/321992.321997","volume":"24","author":"JA Goguen","year":"1977","unstructured":"Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Initial algebra semantics and continuous algebras. J. ACM 24(1), 68\u201395 (1977)","journal-title":"J. ACM"},{"issue":"6","key":"10_CR25","doi-asserted-by":"publisher","first-page":"1169","DOI":"10.1017\/S0960129508007172","volume":"18","author":"J Goubault-Larrecq","year":"2008","unstructured":"Goubault-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. Math. Struct. Comput. Sci. 18(6), 1169\u20131217 (2008)","journal-title":"Math. Struct. Comput. Sci."},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Hofmann, D., Seal, G., Tholen, W. (eds.): Monoidal Topology. A Categorical Approach to Order, Metric, and Topology. No. 153 in Encyclopedia of Mathematics and its Applications. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781107517288"},{"issue":"1\u20132","key":"10_CR27","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.tcs.2004.07.022","volume":"327","author":"J Hughes","year":"2004","unstructured":"Hughes, J., Jacobs, B.: Simulations in coalgebra. Theor. Comput. Sci. 327(1\u20132), 71\u2013108 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20133","key":"10_CR28","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2006.03.013","volume":"357","author":"M Hyland","year":"2006","unstructured":"Hyland, M., Plotkin, G.D., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1\u20133), 70\u201399 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR29","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/j.entcs.2007.02.019","volume":"172","author":"M Hyland","year":"2007","unstructured":"Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. Electr. Notes Theor. Comput. Sci. 172, 437\u2013458 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Johann, P., Simpson, A., Voigtl\u00e4nder, J.: A generic operational metatheory for algebraic effects. In: Proceedings of LICS 2010, pp. 209\u2013218. IEEE Computer Society (2010)","DOI":"10.1109\/LICS.2010.29"},{"key":"10_CR31","unstructured":"Jones, C.: Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, UK (1990)"},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-642-37075-5_10","volume-title":"Foundations of Software Science and Computation Structures","author":"S Katsumata","year":"2013","unstructured":"Katsumata, S., Sato, T.: Preorders on monads and coalgebraic simulations. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 145\u2013160. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_10"},{"key":"10_CR33","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/j.entcs.2011.09.023","volume":"276","author":"V Koutavas","year":"2011","unstructured":"Koutavas, V., Levy, P.B., Sumii, E.: From applicative to environmental bisimulation. Electr. Notes Theor. Comput. Sci. 276, 215\u2013235 (2011)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: Proceedings of POPL 1989, pp. 344\u2013352 (1989)","DOI":"10.1145\/75277.75307"},{"key":"10_CR35","unstructured":"Lassen, S.: Relational reasoning about contexts. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 91\u2013136 (1998)"},{"key":"10_CR36","unstructured":"Lassen, S.: Relational reasoning about functions and nondeterminism. Ph.D. thesis, Department of Computer Science, University of Aarhus, May 1998"},{"key":"10_CR37","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1016\/S1571-0661(04)80083-5","volume":"20","author":"SB Lassen","year":"1999","unstructured":"Lassen, S.B.: Bisimulation in untyped lambda calculus: B\u00f6hm trees and bisimulation up to context. Electr. Notes Theor. Comput. Sci. 20, 346\u2013374 (1999)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR38","unstructured":"Lassen, S.B.: Eager normal form bisimulation. In: Proceedings of LICS 2005, pp. 345\u2013354 (2005)"},{"key":"10_CR39","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/j.entcs.2005.11.068","volume":"155","author":"SB Lassen","year":"2006","unstructured":"Lassen, S.B.: Normal form simulation for McCarthy\u2019s Amb. Electr. Notes Theor. Comput. Sci. 155, 445\u2013465 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR40","unstructured":"Lawvere, W.F.: Functorial semantics of algebraic theories. Ph.D. thesis (2004)"},{"key":"10_CR41","doi-asserted-by":"crossref","unstructured":"Leventis, T.: Probabilistic B\u00f6hm trees and probabilistic separation. In: Proceedings of LICS (2018)","DOI":"10.1145\/3209108.3209126"},{"key":"10_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0029523","volume-title":"$$\\lambda $$ -Calculus and Computer Science Theory","author":"J-J Levy","year":"1975","unstructured":"Levy, J.-J.: An algebraic interpretation of the $$\\lambda $$ $$\\upbeta $$ K-calculus and a labelled $$\\lambda $$ -calculus. In: B\u00f6hm, C. (ed.) $$\\lambda $$ -Calculus and Computer Science Theory. LNCS, vol. 37, pp. 147\u2013165. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/BFb0029523"},{"key":"10_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-19805-2_3","volume-title":"Foundations of Software Science and Computational Structures","author":"PB Levy","year":"2011","unstructured":"Levy, P.B.: Similarity quotients as final coalgebras. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 27\u201341. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_3"},{"issue":"2","key":"10_CR44","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0890-5401(03)00088-9","volume":"185","author":"P Levy","year":"2003","unstructured":"Levy, P., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182\u2013210 (2003)","journal-title":"Inf. Comput."},{"key":"10_CR45","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/0168-0072(83)90030-1","volume":"24","author":"G Longo","year":"1983","unstructured":"Longo, G.: Set-theoretical models of lambda calculus: theories, expansions, isomorphisms. Ann. Pure Appl. Logic 24, 153\u2013188 (1983)","journal-title":"Ann. Pure Appl. Logic"},{"key":"10_CR46","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician","author":"S Mac Lane","year":"1971","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. GTM, vol. 5. Springer, New York (1971). https:\/\/doi.org\/10.1007\/978-1-4612-9839-7"},{"issue":"3","key":"10_CR47","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1017\/S0956796800000125","volume":"1","author":"IA Mason","year":"1991","unstructured":"Mason, I.A., Talcott, C.L.: Equivalence in functional languages with effects. J. Funct. Program. 1(3), 287\u2013327 (1991)","journal-title":"J. Funct. Program."},{"issue":"2","key":"10_CR48","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R Milner","year":"1992","unstructured":"Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119\u2013141 (1992)","journal-title":"Math. Struct. Comput. Sci."},{"key":"10_CR49","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of LICS 1989, pp. 14\u201323. IEEE Computer Society (1989)"},{"issue":"1","key":"10_CR50","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"10_CR51","unstructured":"Morris, J.: Lambda calculus models of programming languages. Ph.D. thesis, MIT (1969)"},{"key":"10_CR52","unstructured":"Ong, C.L.: Non-determinism in a functional setting. In: Proceedings of LICS 1993, pp. 275\u2013286. IEEE Computer Society (1993)"},{"key":"10_CR53","unstructured":"Ong, C.: The lazy lambda calculus: an investigation into the foundations of functional programming. University of London, Imperial College of Science and Technology (1988)"},{"issue":"2","key":"10_CR54","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G Plotkin","year":"1975","unstructured":"Plotkin, G.: Call-by-name, call-by-value and the lambda-calculus. Theoret. Comput. Sci. 1(2), 125\u2013159 (1975)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR55","unstructured":"Plotkin, G.: Lambda-definability and logical relations. Technical report SAI-RM-4. University of Edinburgh, School of A.I. (1973)"},{"key":"10_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45315-6_1","volume-title":"Foundations of Software Science and Computation Structures","author":"G Plotkin","year":"2001","unstructured":"Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 1\u201324. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_1"},{"key":"10_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45931-6_24","volume-title":"Foundations of Software Science and Computation Structures","author":"G Plotkin","year":"2002","unstructured":"Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_24"},{"issue":"1","key":"10_CR58","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1023064908962","volume":"11","author":"GD Plotkin","year":"2003","unstructured":"Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categorical Struct. 11(1), 69\u201394 (2003)","journal-title":"Appl. Categorical Struct."},{"issue":"4","key":"10_CR59","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(4:23)2013","volume":"9","author":"GD Plotkin","year":"2013","unstructured":"Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Logical Methods Comput. Sci. 9(4), 1\u201336 (2013)","journal-title":"Logical Methods Comput. Sci."},{"key":"10_CR60","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"D Pous","year":"2012","unstructured":"Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, New York (2012)"},{"key":"10_CR61","unstructured":"Reynolds, J.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513\u2013523 (1983)"},{"key":"10_CR62","unstructured":"Sands, D.: Improvement theory and its applications. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 275\u2013306. Publications of the Newton Institute, Cambridge University Press (1998)"},{"issue":"1","key":"10_CR63","doi-asserted-by":"publisher","first-page":"5: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), 5:1\u20135:69 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-57208-2_10","volume-title":"CONCUR\u201993","author":"D Sangiorgi","year":"1993","unstructured":"Sangiorgi, D.: A theory of bisimulation for the $$\\phi $$ -calculus. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 127\u2013142. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_10"},{"issue":"1","key":"10_CR65","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1994.1042","volume":"111","author":"D Sangiorgi","year":"1994","unstructured":"Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. Inf. Comput. 111(1), 120\u2013153 (1994)","journal-title":"Inf. Comput."},{"key":"10_CR66","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D., Vignudelli, V.: Environmental bisimulations for probabilistic higher-order languages. In: Proceedings of POPL 2016, pp. 595\u2013607 (2016)","DOI":"10.1145\/2914770.2837651"},{"key":"10_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-319-89884-1_11","volume-title":"Programming Languages and Systems","author":"A Simpson","year":"2018","unstructured":"Simpson, A., Voorneveld, N.: Behavioural equivalence via modalities for algebraic effects. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 300\u2013326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_11"},{"key":"10_CR68","doi-asserted-by":"crossref","unstructured":"St\u00f8vring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: Proceedings of POPL 2007, pp. 161\u2013172 (2007)","DOI":"10.1145\/1190215.1190244"},{"issue":"2","key":"10_CR69","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1214\/aoms\/1177700153","volume":"36","author":"V Strassen","year":"1965","unstructured":"Strassen, V.: The existence of probability measures with given marginals. Ann. Math. Statist. 36(2), 423\u2013439 (1965)","journal-title":"Ann. Math. Statist."},{"issue":"2","key":"10_CR70","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pacific J. Math."},{"key":"10_CR71","unstructured":"Thijs, A.: Simulation and fixpoint semantics. Rijksuniversiteit Groningen (1996)"},{"key":"10_CR72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71050-9","volume-title":"Optimal Transport: Old and New. Grundlehren der mathematischen Wissenschaften","author":"C Villani","year":"2008","unstructured":"Villani, C.: Optimal Transport: Old and New. Grundlehren der mathematischen Wissenschaften. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71050-9"},{"key":"10_CR73","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Monads for functional programming. In: Program Design Calculi, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, 28 July \u2013 9 August 1992, pp. 233\u2013264 (1992)","DOI":"10.1007\/978-3-662-02880-3_8"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17184-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,16]],"date-time":"2024-07-16T17:46:44Z","timestamp":1721152004000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17184-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171834","9783030171841"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17184-1_10","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":"6 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","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":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/esop","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":"86","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":"28","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":"33% - 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,2","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":"12","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)"}}]}}