{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:01:28Z","timestamp":1743076888959,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031664373"},{"type":"electronic","value":"9783031664380"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66438-0_3","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"44-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Preorder-Constrained Simulations for\u00a0Program Refinement with\u00a0Effects"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0454-6900","authenticated-orcid":false,"given":"Koko","family":"Muroya","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3409-6963","authenticated-orcid":false,"given":"Takahiro","family":"Sanada","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1554-6618","authenticated-orcid":false,"given":"Natsuki","family":"Urabe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"3_CR1","unstructured":"Abramsky, S.: The lazy lambda-calculus, pp. 65\u2013117. Addison Wesley (1990)"},{"key":"3_CR2","series-title":"NATO Science Series","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-94-010-0413-8_2","volume-title":"Proof and System-Reliability","author":"S Abramsky","year":"2002","unstructured":"Abramsky, S.: Algorithmic game semantics. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability. NATO Science Series, vol. 62, pp. 21\u201347. Springer, Dordrecht (2002). https:\/\/doi.org\/10.1007\/978-94-010-0413-8_2"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP 2014, pp. 363\u2013376. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628154","DOI":"10.1145\/2628136.2628154"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Dal Lago, U., Vanoni, G.: The machinery of interaction. In: PPDP 2020: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9\u201310 September 2020, pp. 4:1\u20134:15. ACM (2020). https:\/\/doi.org\/10.1145\/3414080.3414108","DOI":"10.1145\/3414080.3414108"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-15205-4_30","volume-title":"Computer Science Logic","author":"B Accattoli","year":"2010","unstructured":"Accattoli, B., Kesner, D.: The structural $$\\lambda $$-calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381\u2013395. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_30"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Bisping, B., Jansen, D.N., Nestmann, U.: Deciding all behavioral equivalences at once: a game for linear-time-branching-time spectroscopy. Log. Methods Comput. Sci. 18(3) (2022). https:\/\/doi.org\/10.46298\/lmcs-18(3:19)2022","DOI":"10.46298\/lmcs-18(3:19)2022"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"de Frutos-Escrig, D., Gregorio-Rodr\u00edguez, C., Palomino, M., Romero-Hern\u00e1ndez, D.: Unifying the linear time-branching time spectrum of process semantics. Log. Methods Comput. Sci. 9(2) (2013). https:\/\/doi.org\/10.2168\/LMCS-9(2:11)2013","DOI":"10.2168\/LMCS-9(2:11)2013"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"de\u00a0Frutos-Escrig, D., Gregorio-Rodr\u00edguez, C.: Constrained simulations, nested simulation semantics and counting bisimulations. In: Pimentel, E. (ed.) Proceedings of the Seventh Spanish Conference on Programming and Computer Languages, PROLE 2007, Zaragoza, Spain, 12\u201314 September 2007. Electronic Notes in Theoretical Computer Science, vol.\u00a0206, pp. 41\u201358. Elsevier (2007). https:\/\/doi.org\/10.1016\/j.entcs.2008.03.074","DOI":"10.1016\/j.entcs.2008.03.074"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0039066","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"RJ Glabbeek","year":"1990","unstructured":"Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278\u2013297. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039066"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"RJ Glabbeek","year":"1993","unstructured":"Glabbeek, R.J.: The linear time \u2014 branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66\u201381. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_6"},{"issue":"1\u20132","key":"3_CR11","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). https:\/\/doi.org\/10.1016\/j.tcs.2004.07.022","journal-title":"Theor. Comput. Sci."},{"key":"3_CR12","unstructured":"Hutagalung, M.: Buffered Simulation for B\u00fcchi Automata. Ph.D. thesis, University of Kassel, Germany (2019). https:\/\/kobra.uni-kassel.de\/bitstream\/handle\/123456789\/11329\/DissertationMilkaHutagalung.pdf?sequence=7 &isAllowed=y"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Hutagalung, M., Lange, M., Lozes, \u00c9.: Buffered simulation games for b\u00fcchi automata. In: \u00c9sik, Z., F\u00fcl\u00f6p, Z. (eds.) Proceedings 14th International Conference on Automata and Formal Languages, AFL 2014, Szeged, Hungary, 27\u201329 May 2014. EPTCS, vol.\u00a0151, pp. 286\u2013300 (2014). https:\/\/doi.org\/10.4204\/EPTCS.151.20","DOI":"10.4204\/EPTCS.151.20"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Johann, P., Simpson, A., Voigtl\u00e4nder, J.: A generic operational metatheory for algebraic effects. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11\u201314 July 2010, Edinburgh, United Kingdom, pp. 209\u2013218. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.29","DOI":"10.1109\/LICS.2010.29"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS 1991), Amsterdam, The Netherlands, 15\u201318 July 1991, pp. 266\u2013277. IEEE Computer Society (1991). https:\/\/doi.org\/10.1109\/LICS.1991.151651","DOI":"10.1109\/LICS.1991.151651"},{"issue":"2","key":"3_CR16","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10703-012-0173-1","volume":"43","author":"S Kiefer","year":"2013","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Algorithmic probabilistic game semantics - playing games with automata. Formal Methods Syst. Des. 43(2), 285\u2013312 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0173-1","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Koutavas, V., Levy, P.B., Sumii, E.: From applicative to environmental bisimulation. In: Mislove, M.W., Ouaknine, J. (eds.) Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, 25\u201328 May 2011. Electronic Notes in Theoretical Computer Science, vol.\u00a0276, pp. 215\u2013235. Elsevier (2011). https:\/\/doi.org\/10.1016\/j.entcs.2011.09.023","DOI":"10.1016\/j.entcs.2011.09.023"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1051\/ita:2005039","volume":"40","author":"D Kuske","year":"2006","unstructured":"Kuske, D.: Theories of orders on the set of words. RAIRO Theor. Inform. Appl. 40(1), 53\u201374 (2006). https:\/\/doi.org\/10.1051\/ita:2005039","journal-title":"RAIRO Theor. Inform. Appl."},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-030-17127-8_20","volume-title":"Foundations of Software Science and Computation Structures","author":"D Kuske","year":"2019","unstructured":"Kuske, D., Zetzsche, G.: Languages ordered by the subword order. In: Boja\u0144czyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 348\u2013364. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17127-8_20"},{"issue":"1","key":"3_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90030-6","journal-title":"Inf. Comput."},{"key":"3_CR21","unstructured":"Morris Jr, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology (1969). https:\/\/dspace.mit.edu\/handle\/1721.1\/64850"},{"key":"3_CR22","unstructured":"Muroya, K.: Hypernet semantics of programming languages. Ph.D. thesis, University of Birmingham, UK (2020). http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.817915"},{"key":"3_CR23","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":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1007\/11523468_59","volume-title":"Automata, Languages and Programming","author":"D Pous","year":"2005","unstructured":"Pous, D.: Up-to techniques for weak bisimulation. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 730\u2013741. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11523468_59"},{"issue":"1\u20132","key":"3_CR25","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.tcs.2007.02.060","volume":"380","author":"D Pous","year":"2007","unstructured":"Pous, D.: New up-to techniques for weak bisimulation. Theor. Comput. Sci. 380(1\u20132), 164\u2013180 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2007.02.060","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"3_CR26","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0960129598002527","volume":"8","author":"D Sangiorgi","year":"1998","unstructured":"Sangiorgi, D.: On the bisimulation proof method. Math. Struct. Comput. Sci. 8(5), 447\u2013479 (1998). https:\/\/doi.org\/10.1017\/S0960129598002527","journal-title":"Math. Struct. Comput. Sci."},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Sangiorgi, D.: Equations, contractions, and unique solutions. ACM Trans. Comput. Log. 18(1), 4:1\u20134:30 (2017). https:\/\/doi.org\/10.1145\/2971339","DOI":"10.1145\/2971339"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/BFb0084781","volume-title":"CONCUR \u201992","author":"D Sangiorgi","year":"1992","unstructured":"Sangiorgi, D., Milner, R.: The problem of \u201cweak bisimulation up to\u2019\u2019. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 32\u201346. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0084781"},{"key":"3_CR29","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":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-61064-2_46","volume-title":"Trees in Algebra and Programming \u2014 CAAP \u201996","author":"J Tiuryn","year":"1996","unstructured":"Tiuryn, J., Wand, M.: Untyped lambda-calculus with input-output. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 317\u2013329. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61064-2_46"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-662-44584-6_31","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"N Urabe","year":"2014","unstructured":"Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative simulations by matrices. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 451\u2013466. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_31"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-47958-3_10","volume-title":"Programming Languages and Systems","author":"T Yachi","year":"2016","unstructured":"Yachi, T., Sumii, E.: A sound and complete bisimulation for contextual equivalence in $$\\lambda $$-calculus with call\/cc. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 171\u2013186. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_10"}],"container-title":["Lecture Notes in Computer Science","Coalgebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66438-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:09:08Z","timestamp":1721891348000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66438-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031664373","9783031664380"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66438-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CMCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Coalgebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cmcs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.coalg.org\/cmcs24\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}