{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T20:31:34Z","timestamp":1792787494678,"version":"4.5.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"DFG, German Research Foundation","award":["470467389"],"award-info":[{"award-number":["470467389"]}],"id":[{"id":"https:\/\/ror.org\/018mejw64","id-type":"ROR","asserted-by":"crossref"}]},{"name":"DFG, German Research Foundation","award":["569130867"],"award-info":[{"award-number":["569130867"]}],"id":[{"id":"https:\/\/ror.org\/018mejw64","id-type":"ROR","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>\n                    Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, the correctness of the corresponding algorithms follows\n                    <jats:italic toggle=\"yes\">intrinsically<\/jats:italic>\n                    just from the type of the computed maps. However, proving recursivity of the underlying coalgebras is non-trivial, and proofs are typically ad hoc. This layer of complexity impedes the formalization of coalgebraically defined recursive algorithms in proof assistants. We introduce a framework for constructing coalgebras which are\n                    <jats:italic toggle=\"yes\">intrinsically<\/jats:italic>\n                    recursive in the sense that the type of the coalgebra guarantees recursivity from the outset. Our approach is based on the novel concept of a\n                    <jats:italic toggle=\"yes\">well-founded functor<\/jats:italic>\n                    on a category of families indexed by a well-founded relation. We show as our main result that every coalgebra for a well-founded functor is recursive, and demonstrate that well-known techniques for proving recursivity and termination such as ranking functions are subsumed by this abstract setup. We present a number of case studies, including Quicksort, the Euclidian algorithm, and CYK parsing. Both the main theoretical result and selected case studies have been formalized in Cubical Agda.\n                  <\/jats:p>","DOI":"10.1145\/3808309","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"1560-1582","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Intrinsically Correct Algorithms and Recursive Coalgebras"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-5210-2873","authenticated-orcid":false,"given":"Cass","family":"Alexandru","sequence":"first","affiliation":[{"name":"RPTU Kaiserslautern-Landau, Department of Computer Science, Kaiserslautern, Germany"},{"name":"Radboud University, Department of Software Science, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3265-7168","authenticated-orcid":false,"given":"Henning","family":"Urbat","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander University Erlangen-N\u00fcrnberg, Department of Computer Science, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8993-6486","authenticated-orcid":false,"given":"Thorsten","family":"Wi\u00dfmann","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander University Erlangen-N\u00fcrnberg, Department of Computer Science, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_3_2_3_2","unstructured":"Ji\u0159\u00ed Ad\u00e1mek Horst Herrlich and George E. Strecker . 2004. Abstract and concrete categories. the joy of cats. (2004)."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108884112"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/575450"},{"key":"e_1_3_2_6_2","unstructured":"The Agda Team . 2025. Function definitions : dot patterns - Agda 2.8.0 documentation. Retrieved Nov. 13 2025 from https:\/\/agda.readthedocs.io\/en\/v2.8.0\/language\/function-definitions.html#dot-patterns."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"[SW] Cass Alexandru Vikraman Choudhury Jurriaan Rot and Niels van der Weide Formalization accompanying the paper \"Intrinsically Correct Sorting in Cubical Agda\" version v0.1 Dec. 2024. doi:10.5281\/zenodo.14279034 URL: https:\/\/doi.org\/10.5281\/zenodo.14279034.","DOI":"10.5281\/zenodo.14279034"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3703595.3705873"},{"key":"e_1_3_2_9_2","unstructured":"[SW Rel.] Cass Alexandru Henning Urbat and Thorsten Wi\u00dfmann Agda Formalization of \"Intrinsically Correct Algorithms and Recursive Coalgebras\" version v2 Apr. 17 2026. vcs: https:\/\/git8.cs.fau.de\/software\/intrinsically-recursive.git swhid: swh:1:rev:834097b85b85437dac7006910c0e3729368bda63;origin=https:\/\/git8.cs.fau.de\/software\/intrinsically-recursive;visit=swh:1:snp:0de144c92d0e36da95f53f994c7d347d4d43efa47."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"[SW] Cass Alexandru Henning Urbat and Thorsten Wi\u00dfmann Agda Formalization of \"Intrinsically Correct Algorithms and Recursive Coalgebras\" Apr. 2026. doi:10.5281\/zenodo.19628996 URL: https:\/\/zenodo.org\/records\/19628996.","DOI":"10.5281\/zenodo.19628996"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/2060081"},{"key":"e_1_3_2_12_2","isbn-type":"print","volume-title":"Algebra of Programming. Prentice Hall International Series in Computer Science","author":"Bird Richard S.","year":"1997","unstructured":"Richard S. Bird and Oege de Moor . 1997. Algebra of Programming. Prentice Hall International Series in Computer Science. Prentice Hall. isbn 78-0-13-507245-5.","ISBN":"https:\/\/id.crossref.org\/isbn\/780135072455"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.08.005"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2025.32"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_2_18_2","unstructured":"Adam Eppendahl . Fixed Point Objects Corresponding to Freyd Algebras. (May 2000)."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"[SW] Hugo Herbelin Rocq-Prover\/Rocq: Rocq 9.1.1 Feb. 2026. doi:10.5281\/zenodo.18554917 URL: https:\/\/zenodo.org\/records\/18554917.","DOI":"10.5281\/zenodo.18554917"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676989"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/5.1.10"},{"key":"e_1_3_2_22_2","isbn-type":"print","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft John E.","year":"1979","unstructured":"John E. Hopcroft and Jeffrey D. Ullman . 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, MA. isbn: 978-0201029888.","ISBN":"https:\/\/id.crossref.org\/isbn\/9780201029888"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000481"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1112\/blms\/14.4.285"},{"key":"e_1_3_2_25_2","isbn-type":"print","volume-title":"The Art of Computer Programming, Volume 2: Seminumerical Algorithms","author":"Knuth Donald E.","year":"1997","unstructured":"Donald E. Knuth . 1997. The Art of Computer Programming, Volume 2: Seminumerical Algorithms. (3rd ed.). Addison-Wesley, Reading, Massachusetts. isbn: 978-0-201-89684-8.","ISBN":"https:\/\/id.crossref.org\/isbn\/9780201896848","edition":"3"},{"key":"e_1_3_2_26_2","unstructured":"Xavier Leroy . 2024. Well-founded recursion done right. In CoqPL 2024: The Tenth International Workshop on Coq for Programming Languages. ACM London United Kingdom (Jan. 2024). https:\/\/inria.hal.science\/hal-04356563."},{"key":"e_1_3_2_27_2","volume-title":"Categories for the Working Mathematician","author":"Mac Lane Saunders","year":"1998","unstructured":"Saunders Mac Lane . 1998. Categories for the Working Mathematician. (2nd ed.). Graduate Texts in Mathematics. Vol. 5. Springer.","edition":"2"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_7"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(74)90032-2"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729281"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:9)2013"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.2307\/3621547"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2026.24"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808309","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:46:36Z","timestamp":1790073996000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808309"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":34,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808309"],"URL":"https:\/\/doi.org\/10.1145\/3808309","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}