Intrinsically Correct Algorithms and Recursive Coalgebras

Alexandru C, Urbat H, Wißmann T (2026)

Publication Type: Journal article

Publication year: 2026

Journal

Proceedings of the ACM on Programming Languages Association for Computing Machinery (ACM)

Book Volume: 10

Pages Range: 1560 - 1582

Article Number: 231

DOI: 10.1145/3808309

Abstract

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 intrinsically 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 intrinsically 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 well-founded functor 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.

Authors with CRIS profile

Henning Urbat Lehrstuhl für Informatik 8 (Theoretische Informatik) Thorsten Wißmann Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau (RPTU) DE Germany (DE)

How to cite

APA:

Alexandru, C., Urbat, H., & Wißmann, T. (2026). Intrinsically Correct Algorithms and Recursive Coalgebras. Proceedings of the ACM on Programming Languages, 10, 1560 - 1582. https://doi.org/10.1145/3808309

MLA:

Alexandru, Cass, Henning Urbat, and Thorsten Wißmann. "Intrinsically Correct Algorithms and Recursive Coalgebras." Proceedings of the ACM on Programming Languages 10 (2026): 1560 - 1582.

BibTeX: Download