{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:33:11Z","timestamp":1767929591806,"version":"3.49.0"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572302","type":"print"},{"value":"9783031572319","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We start with the observation that logical predicates are special cases of <jats:italic>coalgebraic invariants<\/jats:italic> on mixed-variance functors. We then introduce the notion of a <jats:italic>locally maximal logical refinement<\/jats:italic> of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part.<\/jats:p>","DOI":"10.1007\/978-3-031-57231-9_3","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T18:01:54Z","timestamp":1712340114000},"page":"47-69","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Logical Predicates in Higher-Order Mathematical Operational Semantics"],"prefix":"10.1007","author":[{"given":"Sergey","family":"Goncharov","sequence":"first","affiliation":[]},{"given":"Alessio","family":"Santamaria","sequence":"additional","affiliation":[]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]},{"given":"Stelios","family":"Tsampas","sequence":"additional","affiliation":[]},{"given":"Henning","family":"Urbat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"3_CR1","unstructured":"Abramsky, S.: The lazy $$\\lambda $$-calculus. In: Research topics in Functional Programming, pp. 65\u2013117. Addison Wesley (1990)"},{"key":"3_CR2","unstructured":"Ad\u00e1mek, J., Herrlich, H., Strecker, G.E.: Abstract and Concrete Categories. Wiley (1990), republished in: Reprints in Theory and Applications of Categories 17 (2006), pp. 1-507, http:\/\/www.tac.mta.ca\/tac\/reprints\/articles\/17\/tr17abs.html"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Ad\u00e1mek, J., Rosick\u00fd, J.: Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series, Cambridge University Press (1994). https:\/\/doi.org\/10.1017\/CBO9780511600579","DOI":"10.1017\/CBO9780511600579"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Birkedal, L.: Step-indexed logical relations for countable nondeterminism and probabilistic choice. In: 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023). Proc. ACM Program. Lang., vol.\u00a07. ACM (2023). https:\/\/doi.org\/10.1145\/3571195","DOI":"10.1145\/3571195"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: 15th European Symposium on Programming (ESOP 2006). LNCS, vol.\u00a03924, pp. 69\u201383. Springer (2006). https:\/\/doi.org\/10.1007\/11693024_6","DOI":"10.1007\/11693024_6"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Kaposi, A.: Normalisation by evaluation for dependent types. In: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). LIPIcs, vol.\u00a052, pp. 6:1\u20136:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.6","DOI":"10.4230\/LIPIcs.FSCD.2016.6"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001). https:\/\/doi.org\/10.1145\/504709.504712","DOI":"10.1145\/504709.504712"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Benton, N., Hur, C.K.: Biorthogonality, step-indexing and compiler correctness. In: 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009). p. 97\u2013108. ACM (2009). https:\/\/doi.org\/10.1145\/1596550.1596567","DOI":"10.1145\/1596550.1596567"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: The category-theoretic solution of recursive metric-space equations. Theoretical Computer Science 411(47), 4102\u20134122 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.07.010","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Pitts, A. (ed.) 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015). LNCS, vol.\u00a09034, pp. 279\u2013294. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Borceux, F.: Handbook of Categorical Algebra: Volume 1: Basic Category Theory, Encyclopedia of Mathematics and Its Applications, vol.\u00a01. Cambridge University Press (1994). https:\/\/doi.org\/10.1017\/CBO9780511525858","DOI":"10.1017\/CBO9780511525858"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Carboni, A., Lack, S., Walters, R.F.C.: Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra 84(2), 145\u2013158 (Feb 1993). https:\/\/doi.org\/10.1016\/0022-4049(93)90035-R","DOI":"10.1016\/0022-4049(93)90035-R"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Dagnino, F., Gavazzo, F.: A fibrational tale of operational logical relations. In: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). LIPIcs, vol.\u00a0228, pp. 3:1\u20133:21. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2022.3","DOI":"10.4230\/LIPIcs.FSCD.2022.3"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Dagnino, F., Gavazzo, F.: A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential. CoRR (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.03271","DOI":"10.48550\/arXiv.2303.03271"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Gavazzo, F.: Differential logical relations, part ii increments and derivatives. Theor. Comput. Sci. 895(C), 34\u201347 (2021). https:\/\/doi.org\/10.1016\/j.tcs.2021.09.027","DOI":"10.1016\/j.tcs.2021.09.027"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Gavazzo, F., Levy, P.B.: Effectful applicative bisimilarity: Monads, relators, and Howe\u2019s method. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2017). pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005117","DOI":"10.1109\/LICS.2017.8005117"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Dreyer, D., Ahmed, A., Birkedal, L.: Logical step-indexed logical relations. In: 24th Annual IEEE Symposium on Logic In Computer Science (LICS 2009). pp. 71\u201380. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/LICS.2009.34","DOI":"10.1109\/LICS.2009.34"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. Math. Struct. Comput. Sci. 32(8), 1028\u20131065 (2022). https:\/\/doi.org\/10.1017\/S0960129522000263","DOI":"10.1017\/S0960129522000263"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999). pp. 193\u2013202. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782615","DOI":"10.1109\/LICS.1999.782615"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Fiore, M.P., Turi, D.: Semantics of name and value passing. In: 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001). pp. 93\u2013104. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932486","DOI":"10.1109\/LICS.2001.932486"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Georges, A.L., Gu\u00e9neau, A., Van\u00a0Strydonck, T., Timany, A., Trieu, A., Devriese, D., Birkedal, L.: Cerise: Program verification on a capability machine in the presence of untrusted code. J. ACM (2023). https:\/\/doi.org\/10.1145\/3623510","DOI":"10.1145\/3623510"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Giarrusso, P.G., Stefanesco, L., Timany, A., Birkedal, L., Krebbers, R.: Scala step-by-step: Soundness for dot with step-indexed logical relations in iris. In: 25th ACM SIGPLAN International Conference on Functional Programming (ICFP 2020). Proc. ACM Program. Lang., vol.\u00a04. ACM (2020). https:\/\/doi.org\/10.1145\/3408996","DOI":"10.1145\/3408996"},{"key":"3_CR23","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and types, vol.\u00a07. Cambridge University Press (1989)"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Goncharov, S., Milius, S., Schr\u00f6der, L., Tsampas, S., Urbat, H.: Towards a higher-order mathematical operational semantics. In: 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023). Proc. ACM Program. Lang., vol.\u00a07. ACM (2023). https:\/\/doi.org\/10.1145\/3571215","DOI":"10.1145\/3571215"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Goncharov, S., Santamaria, A., Schr\u00f6der, L., Tsampas, S., Urbat, H.: Logical predicates in higher-order mathematical operational semantics (2024), https:\/\/arxiv.org\/abs\/2401.05872","DOI":"10.1007\/978-3-031-57231-9_3"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Gordon, A.D.: Bisimilarity as a theory of functional programming. Theor. Comput. Sci. 228(1-2), 5\u201347 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00353-3","DOI":"10.1016\/S0304-3975(98)00353-3"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Goubault-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. Math. Struct. Comput. Sci. 18(6), 1169\u20131217 (2008). https:\/\/doi.org\/10.1017\/S0960129508007172","DOI":"10.1017\/S0960129508007172"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Hermida, C., Reddy, U.S., Robinson, E.P.: Logical relations and parametricity - A Reynolds programme for category theory and programming languages. Electron. Notes Theor. Comput. Sci. 303, 149\u2013180 (2014). https:\/\/doi.org\/10.1016\/j.entcs.2014.02.008","DOI":"10.1016\/j.entcs.2014.02.008"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Hermida, C.A.: Fibrations, logical predicates and indeterminates. Ph.D. thesis, University of Edinburgh (1993), https:\/\/era.ed.ac.uk\/handle\/1842\/14057","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Hindley, J.R., Seldin, J.P.: Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, 2 edn. (2008). https:\/\/doi.org\/10.1017\/CBO9780511809835","DOI":"10.1017\/CBO9780511809835"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Howe, D.J.: Equality in lazy computation systems. In: 4th Annual Symposium on Logic in Computer Science (LICS 1989). pp. 198\u2013203. IEEE Computer Society (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39174","DOI":"10.1109\/LICS.1989.39174"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103\u2013112 (1996). https:\/\/doi.org\/10.1006\/inco.1996.0008","DOI":"10.1006\/inco.1996.0008"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Hur, C.K., Dreyer, D.: A Kripke Logical Relation between ML and Assembly. In: 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2023). p. 133\u2013146. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926402","DOI":"10.1145\/1926385.1926402"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Hur, C.K., Dreyer, D., Neis, G., Vafeiadis, V.: The Marriage of Bisimulations and Kripke Logical Relations. In: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012). SIGPLAN Not., vol.\u00a047, p. 59\u201372. ACM (2012). https:\/\/doi.org\/10.1145\/2103621.2103666","DOI":"10.1145\/2103621.2103666"},{"key":"3_CR35","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. No.\u00a0141 in Studies in Logic and the Foundations of Mathematics, North Holland (1999)"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation, Cambridge Tracts in Theoretical Computer Science, vol.\u00a059. Cambridge University Press (2016). https:\/\/doi.org\/10.1017\/CBO9781316823187","DOI":"10.1017\/CBO9781316823187"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Johann, P., Simpson, A., Voigtl\u00e4nder, J.: A generic operational metatheory for algebraic effects. In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010). pp. 209\u2013218. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.29","DOI":"10.1109\/LICS.2010.29"},{"key":"3_CR38","unstructured":"Katsumata, S.: A generalisation of pre-logical predicates and its applications. Ph.D. thesis, University of Edinburgh (2005), http:\/\/hdl.handle.net\/1842\/850"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Kurz, A., Velebil, J.: Relation lifting, a survey. Journal of Logical and Algebraic Methods in Programming 85(4), 475\u2013499 (2016). https:\/\/doi.org\/10.1016\/j.jlamp.2015.08.002","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Lago, U.D., Gavazzo, F.: Effectful program distancing. In: 49th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022). Proc. ACM Program. Lang., vol.\u00a06, pp. 1\u201330 (2022). https:\/\/doi.org\/10.1145\/3498680","DOI":"10.1145\/3498680"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Lago, U.D., Gavazzo, F., Yoshimizu, A.: Differential Logical Relations, Part I: The Simply-Typed Case. In: 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). LIPIcs, vol.\u00a0132, pp. 111:1\u2013111:14. Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.111","DOI":"10.4230\/LIPIcs.ICALP.2019.111"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Levy, P., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182\u2013210 (2003)","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Mac\u00a0Lane, S.: Categories for the Working Mathematician, Graduate Texts in Mathematics, vol.\u00a05. Springer, 2 edn. (1978), http:\/\/link.springer.com\/10.1007\/978-1-4757-4721-8","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17(3), 348\u2013375 (1978). https:\/\/doi.org\/10.1016\/0022-0000(78)90014-4","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"3_CR45","doi-asserted-by":"publisher","unstructured":"New, M.S., Bowman, W.J., Ahmed, A.: Fully abstract compilation via universal embedding. In: 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). pp. 103\u2013116. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951941","DOI":"10.1145\/2951913.2951941"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W., Riecke, J.G.: Kripke logical relations and PCF. Inf. Comput. 120(1), 107\u2013116 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1103","DOI":"10.1006\/inco.1995.1103"},{"key":"3_CR47","unstructured":"Ong, C.H.L.: The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. Ph.D. thesis, Imperial College London (1988), http:\/\/hdl.handle.net\/10044\/1\/47211"},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Patrignani, M., Martin, E.M., Devriese, D.: On the semantic expressiveness of recursive types. In: 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021). Proc. ACM Program. Lang., vol.\u00a05. ACM (2021). https:\/\/doi.org\/10.1145\/3434302","DOI":"10.1145\/3434302"},{"key":"3_CR49","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press (2002)"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: 11th Annual IEEE Symposium on Logic in Computer Science (LICS 1996). pp. 152\u2013163. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561314","DOI":"10.1109\/LICS.1996.561314"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Relational properties of domains. Information and Computation 127(2), 66\u201390 (1996). https:\/\/doi.org\/10.1006\/inco.1996.0052","DOI":"10.1006\/inco.1996.0052"},{"key":"3_CR52","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10(3), 321\u2013359 (2000). https:\/\/doi.org\/10.1017\/S0960129500003066","DOI":"10.1017\/S0960129500003066"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Pitts, A.M., Stark, I.D.B.: Observable properties of higher order functions that dynamically create local names, or: What\u2019s new? In: 8th International Symposium on Mathematical Foundations of Computer Science (MFCS 1993). LNCS, vol.\u00a0711, pp. 122\u2013141. Springer (1993). https:\/\/doi.org\/10.1007\/3-540-57182-5_8","DOI":"10.1007\/3-540-57182-5_8"},{"key":"3_CR54","unstructured":"Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 227\u2013274. Cambridge University Press, New York, NY, USA (1998)"},{"key":"3_CR55","unstructured":"Plotkin, G.D.: Lambda-definability and logical relations. Tech. rep., University of Edinburgh (1973)"},{"key":"3_CR56","doi-asserted-by":"publisher","unstructured":"Sieber, K.: Reasoning about sequential functions via logical relations. In: Fourman, M.P., Johnstone, P.T., Pitts, A.M. (eds.) Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991. p. 258\u2013269. London Mathematical Society Lecture Note Series, Cambridge University Press (1992). https:\/\/doi.org\/10.1017\/CBO9780511525902.015","DOI":"10.1017\/CBO9780511525902.015"},{"key":"3_CR57","doi-asserted-by":"publisher","unstructured":"Skorstengaard, L.: An Introduction to Logical Relations (2019). https:\/\/doi.org\/10.48550\/arXiv.1907.11133","DOI":"10.48550\/arXiv.1907.11133"},{"key":"3_CR58","doi-asserted-by":"publisher","unstructured":"Statman, R.: Logical relations and the typed lambda-calculus. Information and Control 65(2), 85\u201397 (1985). https:\/\/doi.org\/10.1016\/S0019-9958(85)80001-2","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"3_CR59","doi-asserted-by":"publisher","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198\u2013212 (1967). https:\/\/doi.org\/10.2307\/2271658","DOI":"10.2307\/2271658"},{"key":"3_CR60","doi-asserted-by":"publisher","unstructured":"Timany, A., Stefanesco, L., Krogh-Jespersen, M., Birkedal, L.: A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runst. In: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). Proc. ACM Program. Lang., vol.\u00a02. ACM (2017). https:\/\/doi.org\/10.1145\/3158152","DOI":"10.1145\/3158152"},{"key":"3_CR61","doi-asserted-by":"publisher","unstructured":"Turi, D., Plotkin, G.D.: Towards a mathematical operational semantics. In: 12th Annual IEEE Symposium on Logic in Computer Science (LICS 1997). pp. 280\u2013291 (1997). https:\/\/doi.org\/10.1109\/LICS.1997.614955","DOI":"10.1109\/LICS.1997.614955"},{"key":"3_CR62","doi-asserted-by":"publisher","unstructured":"Urbat, H., Tsampas, S., Goncharov, S., Milius, S., Schr\u00f6der, L.: Weak similarity in higher-order mathematical operational semantics. In: 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2023). IEEE Computer Society Press (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175706","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"3_CR63","doi-asserted-by":"publisher","unstructured":"Wand, M., Culpepper, R., Giannakopoulos, T., Cobb, A.: Contextual equivalence for a probabilistic language with continuous random variables and recursion. In: 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP 2018). Proc. ACM Program. Lang., vol.\u00a02. ACM (2018). https:\/\/doi.org\/10.1145\/3236782","DOI":"10.1145\/3236782"}],"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-031-57231-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T16:03:05Z","timestamp":1714752185000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57231-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572302","9783031572319"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57231-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","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":"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":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fossacs\/","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":"79","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":"24","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":"30% - 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","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":"9","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)"}}]}}