{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T09:05:01Z","timestamp":1787043901788,"version":"build-2736575974"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    Coinduction is a widely used technique for establishing behavioural equivalence of programs in higher-order languages. In recent years, the rise of languages with quantitative (e.g. probabilistic) features has led to extensions of coinductive methods to more refined types of behavioural conformances, most notably notions of behavioural distance. To guarantee soundness of coinductive reasoning, one needs to show that the behavioural conformance at hand forms a program congruence, i.e. it is suitably compatible with the operations of the language. This is usually achieved by a complex proof technique known as\n                    <jats:italic toggle=\"yes\">Howe\u2019s method<\/jats:italic>\n                    , which needs to be carefully adapted to both the specific language and the targeted notion of behavioural conformance. We develop a uniform categorical approach to Howe\u2019s method that features two orthogonal dimensions of abstraction: (1) the underlying higher-order language is modelled by an\n                    <jats:italic toggle=\"yes\">abstract higher-order specification<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">AHOS<\/jats:italic>\n                    ), a novel and very general categorical account of operational semantics, and\n                    <jats:sup>(2)<\/jats:sup>\n                    notions of behavioural conformance (such as relations or metrics) are modelled via fibrations over the base category of an AHOS. Our main result is a fundamental congruence theorem at this level of generality: Under natural conditions on the categorical ingredients and the operational rules of a language modelled by an AHOS, the greatest behavioural (bi)conformance on its operational model forms a congruence. We illustrate our theory by deriving congruence of bisimilarity and behavioural pseudometrics for probabilistic higher-order languages.\n                  <\/jats:p>","DOI":"10.1145\/3776697","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1586-1614","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Higher-Order Behavioural Conformances via Fibrations"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3265-7168","authenticated-orcid":false,"given":"Henning","family":"Urbat","sequence":"first","affiliation":[{"name":"Friedrich-Alexander-University Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"65","volume-title":"Research topics in Functional Programming","author":"Abramsky S.","year":"1990","unstructured":"S. Abramsky. 1990. The lazy \u03bb-calculus. In Research topics in Functional Programming. Addison Wesley, 65-117."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/78162"},{"issue":"3","key":"e_1_3_2_4_2","article-title":"Coalgebraic Behavioral Metrics","volume":"14","author":"Baldan Paolo","year":"2018","unstructured":"Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara Konig. 2018. Coalgebraic Behavioral Metrics. Log. Methods Comput. Sci. 14, 3 (2018).","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.STACS.2024.10"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394738"},{"key":"e_1_3_2_7_2","first-page":"633","volume-title":"In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2015)","author":"Crubill\u00e9 Rapha\u00eblle","year":"2015","unstructured":"Rapha\u00eblle Crubill\u00e9 and Ugo Dal Lago. 2015. Metric reasoning about \u028e-terms: The affine case. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2015). IEEE, 633-644."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-20(2:1)2024"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.111"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_24"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2411.03069"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209149"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571215"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","unstructured":"Sergey Goncharov Stefan Milius Lutz Schroder Stelios Tsampas and Henning Urbat. 2025. Bialgebraic Reasoning on Stateful Languages. arXiv:2503.10955 [cs.PL] https:\/\/arxiv.org\/abs\/2503.10955 To appear in Proc. ICFP 2025.","DOI":"10.1145\/3747513"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662099"},{"key":"e_1_3_2_18_2","doi-asserted-by":"crossref","unstructured":"Sergey Goncharov Pouya Partow and Stelios Tsampas. 2025. Big Steps in Higher-Order Mathematical Operational Semantics. arXiv:2506.01076 [cs.PL] https:\/\/arxiv.org\/abs\/2506.01076 To appear in Proc. ICFP 2025.","DOI":"10.1145\/3747540"},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","unstructured":"Sergey Goncharov Alessio Santamaria Lutz Schr\u00f6der Stelios Tsampas and Henning. 2024. Logical Predicates in Higher-Order Mathematical Operational Semantics. (2024).","DOI":"10.1007\/978-3-031-57231-9_3"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704871"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809835"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:37)2022"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_3_2_26_2","volume-title":"Categorical Logic and Type Theory","author":"Jacobs B.","year":"1999","unstructured":"B. Jacobs. 1999. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782586"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/3470152.3470184"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(93)E0139-P"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.007"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535872"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1051\/ITA\/2012012"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.212"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"e_1_3_2_37_2","volume-title":"Lambda-Calculus Models of Programming Languages","author":"Morris James H.","year":"1968","unstructured":"James H. Morris. 1968. Lambda-Calculus Models of Programming Languages. Ph. D. Dissertation. Massachusetts Institute of Technology."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.006"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.5555\/548945"},{"key":"e_1_3_2_40_2","first-page":"513","article-title":"Types, Abstraction and Parametric Polymorphism","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, Paris, France, September 19-23, 1983. North-Holland\/IFIP, 513-523.","journal-title":"Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-019-00333-X"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110"},{"key":"e_1_3_2_43_2","unstructured":"Henning Urbat. 2025. Higher-Order Behavioural Conformances via Fibrations. arXiv:2507.18509 [cs.PL] https:\/\/arxiv.org\/abs\/2507.18509"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175706"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:40:33Z","timestamp":1784209233000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776697"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776697"],"URL":"https:\/\/doi.org\/10.1145\/3776697","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}