{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:33:13Z","timestamp":1787063593996,"version":"build-2736575974"},"publisher-location":"New York, NY, USA","reference-count":85,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T00:00:00Z","timestamp":1720396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["527481841"],"award-info":[{"award-number":["527481841"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["470467389"],"award-info":[{"award-number":["470467389"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["501369690"],"award-info":[{"award-number":["501369690"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["419850228"],"award-info":[{"award-number":["419850228"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,8]]},"DOI":"10.1145\/3661814.3662099","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T08:30:12Z","timestamp":1718958612000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Bialgebraic Reasoning on Higher-order Program Equivalence"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6924-8766","authenticated-orcid":false,"given":"Sergey","family":"Goncharov","sequence":"first","affiliation":[{"name":"Department of Computer Science, Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2021-1644","authenticated-orcid":false,"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8981-2328","authenticated-orcid":false,"given":"Stelios","family":"Tsampas","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3265-7168","authenticated-orcid":false,"given":"Henning","family":"Urbat","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_6"},{"key":"e_1_3_2_1_2_1","volume-title":"Research topics in Functional Programming","author":"Abramsky S.","unstructured":"S. Abramsky. 1990. The lazy \u03bb-calculus. In Research topics in Functional Programming. Addison Wesley, 65--117."},{"key":"e_1_3_2_1_3_1","volume-title":"Strecker","author":"Ad\u00e1mek Ji\u0159\u00ed","year":"1990","unstructured":"Ji\u0159\u00ed Ad\u00e1mek, Horst Herrlich, and George E. Strecker. 1990. Abstract and Concrete Categories. John Wiley and Sons. Free online version: http:\/\/www.tac.mta.ca\/tac\/reprints\/articles\/17\/tr17abs.html."},{"key":"e_1_3_2_1_4_1","volume-title":"Initial Algebras Without Iteration. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021) (Leibniz International Proceedings in Informatics (LIPIcs)","volume":"20","author":"Ad\u00e1mek Ji\u0159\u00ed","unstructured":"Ji\u0159\u00ed Ad\u00e1mek, Stefan Milius, and Lawrence S. Moss. 2021. Initial Algebras Without Iteration. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 211), Fabio Gadducci and Alexandra Silva (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 5:1--5:20."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_3_2_1_10_1","volume-title":"Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs\/1705.01163","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand and Greg Morrisett. 2017. Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs\/1705.01163 (2017). arXiv:1705.01163 http:\/\/arxiv.org\/abs\/1705.01163"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00152-9"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.240"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525858"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(93)90035-R"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.3"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2303.03271"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.09.027"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837618"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000263"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316083"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_2_1_31_1","volume-title":"CMCS'10 Short Contributions : 10th International Workshop on Coalgebraic Methods in Computer Science.","author":"Marcelo","unstructured":"Marcelo P. Fiore and Sam Staton. 2010. Positive structural operational semantics and monotone distributive law. In CMCS'10 Short Contributions : 10th International Workshop on Coalgebraic Methods in Computer Science."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623510"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408996"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571215"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Sergey Goncharov Stefan Milius Stelios Tsampas and Henning Urbat. 2024. Bialgebraic Reasoning on Higher-Order Program Equivalence. arXiv:2402.00625 [cs.PL]","DOI":"10.1145\/3661814.3662099"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Sergey Goncharov Alessio Santamaria Lutz Schr\u00f6der Stelios Tsampas and Henning Urbat. 2024. Logical Predicates in Higher-Order Mathematical Operational Semantics. (2024).","DOI":"10.1007\/978-3-031-57231-9_3"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00353-3"},{"key":"e_1_3_2_1_38_1","volume-title":"Operational Equivalences for Untyped and Polymorphic Object Calculi","author":"Gordon A. D.","unstructured":"A. D. Gordon. 1999. Operational Equivalences for Untyped and Polymorphic Object Calculi. Cambridge University Press, USA, 9--54."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007172"},{"key":"e_1_3_2_1_40_1","volume-title":"Semantics of Programming Languages: Structures and Techniques","author":"Gunter C.A.","unstructured":"C.A. Gunter. 1992. Semantics of Programming Languages: Structures and Techniques. London."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.02.008"},{"key":"e_1_3_2_1_43_1","volume-title":"logical predicates and indeterminates. Ph. D. Dissertation","author":"Hermida Claudio Alberto","year":"1842","unstructured":"Claudio Alberto Hermida. 1993. Fibrations, logical predicates and indeterminates. Ph. D. Dissertation. University of Edinburgh. https:\/\/era.ed.ac.uk\/handle\/1842\/14057"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809835"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_2_1_51_1","volume-title":"A generalisation of pre-logical predicates and its applications. Ph. D. Dissertation","year":"1842","unstructured":"Shin-ya Katsumata. 2005. A generalisation of pre-logical predicates and its applications. Ph. D. Dissertation. University of Edinburgh. http:\/\/hdl.handle.net\/1842\/850"},{"key":"e_1_3_2_1_52_1","volume-title":"Computer Science Logic - 26th International Workshop\/21st Annual Conference of the EACSL, (CSL 2012) (LIPIcs","author":"Keller Chantal","unstructured":"Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative Sort. In Computer Science Logic - 26th International Workshop\/21st Annual Conference of the EACSL, (CSL 2012) (LIPIcs, Vol. 16), Patrick C\u00e9gielski and Arnaud Durand (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 381--395."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498680"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.111"},{"key":"e_1_3_2_1_55_1","volume-title":"Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation","author":"Lassen S\u00f8ren B.","unstructured":"S\u00f8ren B. Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Aarhus University. https:\/\/www.brics.dk\/DS\/98\/2\/BRICS-DS-98-2.pdf"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_2_1_57_1","volume-title":"Categories for the Working Mathematician (2 ed.). Graduate Texts in Mathematics","author":"Lane S. Mac","unstructured":"S. Mac Lane. 1978. Categories for the Working Mathematician (2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer. http:\/\/link.springer.com\/10.1007\/978-1-4757-4721-8"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1103"},{"key":"e_1_3_2_1_62_1","volume-title":"The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. Ph. D. Dissertation","author":"Luke Ong C-H","unstructured":"C-H Luke Ong. 1988. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. Ph. D. Dissertation. Imperial College London. http:\/\/hdl.handle.net\/10044\/1\/47211"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434302"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561314"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/548945"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055063"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_3_2_1_70_1","volume-title":"Advanced Topics in Types and Programming Languages, Benjamin C","author":"Pitts Andrew M.","unstructured":"Andrew M. Pitts. 2004. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press, Chapter 7."},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57182-5_8"},{"key":"e_1_3_2_1_72_1","volume-title":"Stark","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts and Ian D. B. Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). Cambridge University Press, New York, NY, USA, 227--274."},{"key":"e_1_3_2_1_74_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress, R. E. A. Mason (Ed.). North-Holland\/IFIP, 513--523","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, R. E. A. Mason (Ed.). North-Holland\/IFIP, 513--523."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525902.015"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57201-3_9"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"crossref","unstructured":"Henning Urbat Stelios Tsampas Sergey Goncharov Stefan Milius and Lutz Schr\u00f6der. 2023. Weak Similarity in Higher-Order Mathematical Operational Semantics. arXiv:2302.08200 [cs.PL]","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.036"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80372-4"}],"event":{"name":"LICS '24: 39th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Tallinn Estonia","acronym":"LICS '24","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE Computer Society","EACSL"]},"container-title":["Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662099","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:44:08Z","timestamp":1750275848000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662099"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":85,"alternative-id":["10.1145\/3661814.3662099","10.1145\/3661814"],"URL":"https:\/\/doi.org\/10.1145\/3661814.3662099","relation":{},"subject":[],"published":{"date-parts":[[2024,7,8]]},"assertion":[{"value":"2024-07-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}