{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:28Z","timestamp":1767928648280,"version":"3.49.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["470467389, 419850228"],"award-info":[{"award-number":["470467389, 419850228"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>\n            Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin\u2019s bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin\u2019s framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term\n            <jats:italic>pointed higher-order GSOS laws<\/jats:italic>\n            . We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the \u03bb-calculus w.r.t. a strong variant of Abramsky\u2019s applicative bisimilarity are obtained as instances.\n          <\/jats:p>","DOI":"10.1145\/3571215","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"632-658","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Towards a Higher-Order Mathematical Operational Semantics"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6924-8766","authenticated-orcid":false,"given":"Sergey","family":"Goncharov","sequence":"first","affiliation":[{"name":"University of Erlangen-Nuremberg, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2021-1644","authenticated-orcid":false,"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[{"name":"University of Erlangen-Nuremberg, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[{"name":"University of Erlangen-Nuremberg, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8981-2328","authenticated-orcid":false,"given":"Stelios","family":"Tsampas","sequence":"additional","affiliation":[{"name":"University of Erlangen-Nuremberg, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3265-7168","authenticated-orcid":false,"given":"Henning","family":"Urbat","sequence":"additional","affiliation":[{"name":"University of Erlangen-Nuremberg, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_6"},{"key":"e_1_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\u2013117. S. Abramsky. 1990. The lazy \u03bb -calculus. In Research topics in Functional Programming. Addison Wesley, 65\u2013117."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1044"},{"key":"e_1_2_1_4_1","volume-title":"Algebraic Theories","author":"Ad\u00e1mek Ji\u0159\u00ed","unstructured":"Ji\u0159\u00ed Ad\u00e1mek , Ji\u0159\u00ed Rosick\u00fd , and Enrico Vitale . 2011. Algebraic Theories . Cambridge University Press . Ji\u0159\u00ed Ad\u00e1mek, Ji\u0159\u00ed Rosick\u00fd, and Enrico Vitale. 2011. Algebraic Theories. Cambridge University Press."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394771"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01111838"},{"key":"e_1_2_1_7_1","unstructured":"Falk Bartels. 2004. On generalised coinduction and probabilistic specification formats: Distributive laws in coalgebraic modelling. Ph. D. Dissertation. Vrije Universiteit Amsterdam. \t\t\t\t  Falk Bartels. 2004. On generalised coinduction and probabilistic specification formats: Distributive laws in coalgebraic modelling. Ph. D. Dissertation. Vrije Universiteit Amsterdam."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705652"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00152-9"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200876"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394738"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2307\/2370619"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.38"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.7"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932486"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.30"},{"key":"e_1_2_1_20_1","volume-title":"Andrew D. Gordon and Andrew M. Pitts (Eds.)","unstructured":"1999. Higher Order Operational Techniques in Semantics , Andrew D. Gordon and Andrew M. Pitts (Eds.) . Cambridge University Press , USA. isbn:0521631688 1999. Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). Cambridge University Press, USA. isbn:0521631688"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.02.008"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290334"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:37)2022"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2015.190"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_30"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.15"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.01.012"},{"key":"e_1_2_1_31_1","volume-title":"Communication and concurrency","author":"Milner Robin","unstructured":"Robin Milner . 1989. Communication and concurrency . Prentice Hall . isbn:978-0-13-115007-2 Robin Milner. 1989. Communication and concurrency. Prentice Hall. isbn:978-0-13-115007-2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.09.015"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1103"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.006"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1042"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0096"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.17"},{"key":"e_1_2_1_40_1","volume-title":"Outline of a Mathematical Theory of Computation","author":"Scott Dana","unstructured":"Dana Scott . 1970. Outline of a Mathematical Theory of Computation . Oxford University Computing Laboratory . Dana Scott. 1970. Outline of a Mathematical Theory of Computation. Oxford University Computing Laboratory."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_2_1_42_1","volume-title":"Intensional interpretations of functionals of finite type I. The journal of symbolic logic, 32, 2","author":"Tait William W","year":"1967","unstructured":"William W Tait . 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic, 32, 2 ( 1967 ), 198\u2013212. William W Tait. 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic, 32, 2 (1967), 198\u2013212."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57201-3_9"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2021.88"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.036"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80372-4"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571215","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571215","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571215"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571215"],"URL":"https:\/\/doi.org\/10.1145\/3571215","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}