Intrinsically Correct Algorithms and Recursive Coalgebras

arxiv: 2512.10748 · v3 · submitted 2025-12-11 · 💻 cs.PL · cs.LO

Intrinsically Correct Algorithms and Recursive Coalgebras

Cass Alexandru , Henning Urbat , Thorsten Wi{\ss}mann This is my paper

Pith reviewed 2026-05-16 23:20 UTC · model grok-4.3

classification 💻 cs.PL cs.LO

keywords coalgebrasrecursive algorithmswell-founded functorsterminationindexed familiescategory theoryCubical Agdaprogram correctness

0 comments p. Extension

The pith

Every coalgebra for a well-founded functor on indexed families is recursive, so termination follows from the coalgebra type alone.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs a general setting where recursive algorithms are modeled as coalgebras over categories of families indexed by a well-founded relation. In this setting a functor is called well-founded when it preserves well-foundedness; the central theorem states that every coalgebra for such a functor is automatically recursive. Because recursivity is guaranteed by the type of the coalgebra map, both termination and correctness are obtained without separate proofs. The same abstract condition recovers classical termination arguments such as ranking functions and applies directly to concrete algorithms including Quicksort, the Euclidean algorithm, and CYK parsing. The entire development, including the main theorem and selected examples, has been formalized in Cubical Agda.

Core claim

We show as our main result that every coalgebra for a well-founded functor is recursive. A functor on a category of families indexed by a well-founded relation is well-founded when it maps well-founded objects to well-founded objects; the recursivity condition on a coalgebra then follows directly from this preservation property.

What carries the argument

A well-founded functor on the category of families indexed by a well-founded relation; it preserves well-foundedness and thereby forces every coalgebra to satisfy the recursive equation.

If this is right

Termination and partial correctness of a recursive algorithm become intrinsic properties of its coalgebra type.
Proofs that rely on ranking functions or other well-founded measures are recovered as instances of the same abstract condition.
Algorithms such as Quicksort, the Euclidean algorithm, and CYK parsing receive intrinsic recursive coalgebra structures.
Formalization of recursive algorithms in proof assistants is simplified because no separate termination argument needs to be supplied.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The framework may be applied to other coalgebraic models of recursion that currently require manual well-foundedness proofs.
Dependent type theories could encode the indexing relation directly, allowing the type checker to discharge termination obligations automatically.
Similar well-foundedness preservation conditions might be formulated for other categorical structures such as monads or operads.

Load-bearing premise

The functor must preserve the well-foundedness of families whenever the indexing relation is well-founded.

What would settle it

An explicit coalgebra whose structure map fails the recursive equation while the underlying functor satisfies the well-foundedness preservation condition.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper defines well-founded functors on indexed families so that coalgebras for them are automatically recursive, with the whole thing machine-checked in Cubical Agda.

read the letter

The main takeaway is that they introduce well-founded functors on categories of families indexed by well-founded relations and prove that any coalgebra for one is recursive by construction. The Cubical Agda formalization covers both the theorem and the examples, which removes the usual worry about hidden gaps in the argument. Ranking functions and similar termination tricks fall out as special cases inside this setup rather than separate lemmas. The case studies on Quicksort, the Euclidean algorithm, and CYK parsing are concrete enough to show the idea is usable. What the paper does cleanly is move the termination check into the choice of functor itself, so the type of the coalgebra already guarantees recursivity without extra proof work. That is a genuine simplification for anyone already working in coalgebraic semantics. The soft spot is that you still have to exhibit a suitable well-founded functor for each new algorithm, and the paper does not claim this is always easier than the old ad-hoc proofs. The framework is also tied to well-founded indexing categories, so it will not directly cover every form of recursion without additional setup. This is for readers already comfortable with coalgebras and proof assistants who want a more uniform way to handle recursive definitions. The formalization and the new abstraction are strong enough that it deserves a serious referee rather than a desk reject.

Referee Report

0 major / 2 minor

Summary. The paper introduces well-founded functors on categories of families indexed by well-founded relations. Its central claim is that every coalgebra for a well-founded functor is recursive; this is proved as the main theorem, shown to subsume ranking-function techniques, and illustrated via case studies (Quicksort, Euclidean algorithm, CYK parsing). Both the theorem and selected case studies are fully formalized in Cubical Agda.

Significance. If the result holds, the framework supplies a uniform, intrinsic categorical criterion that guarantees recursivity directly from the coalgebra type, eliminating ad-hoc termination proofs for a class of recursive algorithms. The complete machine-checked formalization in Cubical Agda and the explicit preservation condition on the functor constitute a strong, reproducible contribution that unifies existing termination methods under a single abstract setup.

minor comments (2)

[§3] §3, definition of well-founded functor: the preservation condition is stated clearly but the surrounding prose could explicitly flag that it is an additional hypothesis on the functor rather than a derived property.
[Case studies] Case-study sections: the Agda code excerpts are helpful, yet a short table summarizing which parts of each algorithm are covered by the formalization would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our paper and for recommending acceptance. The summary accurately captures the main contributions: the introduction of well-founded functors on categories of families, the central theorem that every coalgebra for such a functor is recursive, its subsumption of ranking-function techniques, the case studies, and the Cubical Agda formalization.

Circularity Check

0 steps flagged

No circularity; theorem follows from explicit definitions and is machine-verified

full rationale

The central result states that every coalgebra for a well-founded functor (defined via an explicit well-foundedness preservation condition on functors over families indexed by a well-founded relation) is recursive. This is proved directly as a theorem from the stated definitions rather than by construction or tautology. The paper supplies a complete Cubical Agda formalization covering the core theorem and case studies (Quicksort, Euclidean algorithm, CYK), providing independent machine-checked evidence. No load-bearing step reduces to a fitted input, self-citation chain, or renamed ansatz; the derivation remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The framework rests on standard category theory (categories, functors, coalgebras) plus the new definition of well-founded functor. No numerical parameters are fitted. The only invented entity is the well-founded functor itself, which is defined rather than postulated with external evidence.

axioms (2)

domain assumption The base category of families is indexed by a well-founded relation.
Invoked in the definition of the indexed category on which the well-founded functor acts.
standard math Standard properties of coalgebras and recursive coalgebras in a category.
Background from prior coalgebra literature used to state the main theorem.

invented entities (1)

well-founded functor no independent evidence
purpose: A functor on indexed families that preserves well-foundedness so that its coalgebras are automatically recursive.
Defined in the paper as the central new construction; no independent falsifiable prediction is given beyond the theorem itself.

pith-pipeline@v0.9.0 · 5499 in / 1321 out tokens · 22712 ms · 2026-05-16T23:20:06.013531+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat induction / well-founded order recovery echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

We introduce 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 (Theorem 3.7).
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Every well-founded F-coalgebra is recursive (Theorem 2.8, Recursion Theorem for Indexed Sets).

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

[1]

Jiří Adámek, Stefan Milius, and Lawrence S. Moss. 2025.Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors. Cambridge University Press. doi:10.1017/9781108884112

work page doi:10.1017/9781108884112 2025
[2]

2025.Function Definitions : Dot Patterns — Agda 2.8.0 documentation

The Agda Team. 2025.Function Definitions : Dot Patterns — Agda 2.8.0 documentation. https://agda.readthedocs.io/en/ v2.8.0/language/function-definitions.html#dot-patterns

work page 2025
[3]

2024.Intrinsically Correct Sorting in Cubical Agda

Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide. 2024.Intrinsically Correct Sorting in Cubical Agda. doi:10.5281/zenodo.14279034

work page doi:10.5281/zenodo.14279034 2024
[4]

Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide. 2025. Intrinsically Correct Sorting in Cubical Agda. InCertified Programs and Proofs (CPP 2025), Kathrin Stark, Amin Timany, Sandrine Blazy, and Nicolas Tabareau (Eds.). ACM, 34–49. doi:10.1145/3703595.3705873

work page doi:10.1145/3703595.3705873 2025
[5]

2010.Category Theory(2 ed.)

Steve Awodey. 2010.Category Theory(2 ed.). Oxford Logic Guides, Vol. 52. Oxford University Press

work page 2010
[6]

Bird and Oege de Moor

Richard S. Bird and Oege de Moor. 1997.Algebra of Programming. Prentice Hall

work page 1997
[7]

Ana Bove and Venanzio Capretta. 2005. Modelling General Recursion in Type Theory.Mathematical Structures in Computer Science15, 4 (Aug. 2005), 671–708. doi:10.1017/S0960129505004822

work page doi:10.1017/s0960129505004822 2005
[8]

Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. 2006. Recursive coalgebras from comonads.Inf. Comput.204, 4 (2006), 437–468. doi:10.1016/j.ic.2005.08.005

work page doi:10.1016/j.ic.2005.08.005 2006
[9]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination.Commun. ACM54, 5 (May 2011), 88–98. doi:10.1145/1941487.1941509

work page doi:10.1145/1941487.1941509 2011
[10]

Peter Dybjer. 1994. Inductive Families.Formal Aspects of Computing6, 4 (July 1994), 440–465. doi:10.1007/BF01211308

work page doi:10.1007/bf01211308 1994
[11]

Adam Eppendahl. 2000. Fixed Point Objects Corresponding to Freyd Algebras. (May 2000)

work page 2000
[12]

Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. 2015. Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 527–538. doi:10.1145/2676726.2676989

work page doi:10.1145/2676726.2676989 2015
[13]

C. A. R. Hoare. 1962. Quicksort.Comput. J.5, 1 (1962), 10–16. doi:10.1093/comjnl/5.1.10

work page doi:10.1093/comjnl/5.1.10 1962
[14]

Hopcroft and Jeffrey D

John E. Hopcroft and Jeffrey D. Ullman. 1979.Introduction to Automata Theory, Languages, and Computation. Addison- Wesley, Reading, MA

work page 1979
[15]

Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. 2017. Well-Founded Coalgebras, Revisited.Mathematical Structures in Computer Science27, 7 (Oct. 2017), 1111–1131. doi:10.1017/S0960129515000481

work page doi:10.1017/s0960129515000481 2017
[16]

Laurie Kirby and Jeff Paris. 1982. Accessible independence results for Peano arithmetic.Bulletin of the London Mathematical Society14, 4 (1982), 285–293. doi:10.1112/blms/14.4.285

work page doi:10.1112/blms/14.4.285 1982
[17]

Donald E. Knuth. 1997.The Art of Computer Programming, Volume 2: Seminumerical Algorithms(3rd ed.). Addison- Wesley, Reading, Massachusetts

work page 1997
[18]

Xavier Leroy. 2024. Well-Founded Recursion Done Right. InCoqPL 2024: The Tenth International Workshop on Coq for Programming Languages. ACM, London, United Kingdom. https://inria.hal.science/hal-04356563

work page 2024
[19]

1998.Categories for the Working Mathematician(2 ed.)

Saunders Mac Lane. 1998.Categories for the Working Mathematician(2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer

work page 1998
[20]

Fokkinga, and Ross Paterson

Erik Meijer, Maarten M. Fokkinga, and Ross Paterson. 1991. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. InFunctional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings (Lecture Notes in Computer Science, Vol. 523), John Hughes (Ed.). Springer, 124–144. doi:10....

work page doi:10.1007/3540543961_7 1991
[21]

Gerhard Osius. 1974. Categorical Set Theory: A Characterization of the Category of Sets.Journal of Pure and Applied Algebra4, 1 (Feb. 1974), 79–119. doi:10.1016/0022-4049(74)90032-2

work page doi:10.1016/0022-4049(74)90032-2 1974
[22]

Podelski and A

A. Podelski and A. Rybalchenko. 2004. Transition invariants. InProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.32–41. doi:10.1109/LICS.2004.1319598

work page doi:10.1109/lics.2004.1319598 2004
[23]

Intrinsic Verification of 22 Cass Alexandru, Henning Urbat, and Thorsten Wißmann Parsers and Formal Grammar Theory in Dependent Lambek Calculus

Steven Schaefer, Nathan Varner, Pedro Henrique Azevedo de Amorim, and Max S. New. 2025. Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus.Agda Formalization of "Intrinsic Verification of 22 Cass Alexandru, Henning Urbat, and Thorsten Wißmann Parsers and Formal Grammar Theory in Dependent Lambek Calculus"9, PLDI (June...

work page 2025
[24]

Bonsangue, and Jan J

Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. 2013. Generalizing determinization from automata to coalgebras.Logical Methods in Computer Science9, 1 (2013). doi:10.2168/LMCS-9(1:9)2013

work page doi:10.2168/lmcs-9(1:9)2013 2013
[25]

1999.Practical Foundations of Mathematics

Paul Taylor. 1999.Practical Foundations of Mathematics. Cambridge University Press. doi:10.2307/3621547

work page doi:10.2307/3621547 1999
[26]

Henning Urbat and Thorsten Wißmann. 2025. Well-Founded Coalgebras Meet König’s Lemma. arXiv:2507.18539 [cs.LO] https://arxiv.org/abs/2507.18539 To appear in CSL 2026

work page arXiv 2025
[27]

Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types.Proc. ACM Program. Lang.3, ICFP (July 2019), 87:1–87:29. doi:10.1145/3341691 Intrinsically Correct Algorithms and Recursive Coalgebras 23 A Preservation Properties for Recursive Coalgebras We present tw...

work page doi:10.1145/3341691 2019

[1] [1]

Jiří Adámek, Stefan Milius, and Lawrence S. Moss. 2025.Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors. Cambridge University Press. doi:10.1017/9781108884112

work page doi:10.1017/9781108884112 2025

[2] [2]

2025.Function Definitions : Dot Patterns — Agda 2.8.0 documentation

The Agda Team. 2025.Function Definitions : Dot Patterns — Agda 2.8.0 documentation. https://agda.readthedocs.io/en/ v2.8.0/language/function-definitions.html#dot-patterns

work page 2025

[3] [3]

2024.Intrinsically Correct Sorting in Cubical Agda

Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide. 2024.Intrinsically Correct Sorting in Cubical Agda. doi:10.5281/zenodo.14279034

work page doi:10.5281/zenodo.14279034 2024

[4] [4]

Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide. 2025. Intrinsically Correct Sorting in Cubical Agda. InCertified Programs and Proofs (CPP 2025), Kathrin Stark, Amin Timany, Sandrine Blazy, and Nicolas Tabareau (Eds.). ACM, 34–49. doi:10.1145/3703595.3705873

work page doi:10.1145/3703595.3705873 2025

[5] [5]

2010.Category Theory(2 ed.)

Steve Awodey. 2010.Category Theory(2 ed.). Oxford Logic Guides, Vol. 52. Oxford University Press

work page 2010

[6] [6]

Bird and Oege de Moor

Richard S. Bird and Oege de Moor. 1997.Algebra of Programming. Prentice Hall

work page 1997

[7] [7]

Ana Bove and Venanzio Capretta. 2005. Modelling General Recursion in Type Theory.Mathematical Structures in Computer Science15, 4 (Aug. 2005), 671–708. doi:10.1017/S0960129505004822

work page doi:10.1017/s0960129505004822 2005

[8] [8]

Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. 2006. Recursive coalgebras from comonads.Inf. Comput.204, 4 (2006), 437–468. doi:10.1016/j.ic.2005.08.005

work page doi:10.1016/j.ic.2005.08.005 2006

[9] [9]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination.Commun. ACM54, 5 (May 2011), 88–98. doi:10.1145/1941487.1941509

work page doi:10.1145/1941487.1941509 2011

[10] [10]

Peter Dybjer. 1994. Inductive Families.Formal Aspects of Computing6, 4 (July 1994), 440–465. doi:10.1007/BF01211308

work page doi:10.1007/bf01211308 1994

[11] [11]

Adam Eppendahl. 2000. Fixed Point Objects Corresponding to Freyd Algebras. (May 2000)

work page 2000

[12] [12]

Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. 2015. Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 527–538. doi:10.1145/2676726.2676989

work page doi:10.1145/2676726.2676989 2015

[13] [13]

C. A. R. Hoare. 1962. Quicksort.Comput. J.5, 1 (1962), 10–16. doi:10.1093/comjnl/5.1.10

work page doi:10.1093/comjnl/5.1.10 1962

[14] [14]

Hopcroft and Jeffrey D

John E. Hopcroft and Jeffrey D. Ullman. 1979.Introduction to Automata Theory, Languages, and Computation. Addison- Wesley, Reading, MA

work page 1979

[15] [15]

Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. 2017. Well-Founded Coalgebras, Revisited.Mathematical Structures in Computer Science27, 7 (Oct. 2017), 1111–1131. doi:10.1017/S0960129515000481

work page doi:10.1017/s0960129515000481 2017

[16] [16]

Laurie Kirby and Jeff Paris. 1982. Accessible independence results for Peano arithmetic.Bulletin of the London Mathematical Society14, 4 (1982), 285–293. doi:10.1112/blms/14.4.285

work page doi:10.1112/blms/14.4.285 1982

[17] [17]

Donald E. Knuth. 1997.The Art of Computer Programming, Volume 2: Seminumerical Algorithms(3rd ed.). Addison- Wesley, Reading, Massachusetts

work page 1997

[18] [18]

Xavier Leroy. 2024. Well-Founded Recursion Done Right. InCoqPL 2024: The Tenth International Workshop on Coq for Programming Languages. ACM, London, United Kingdom. https://inria.hal.science/hal-04356563

work page 2024

[19] [19]

1998.Categories for the Working Mathematician(2 ed.)

Saunders Mac Lane. 1998.Categories for the Working Mathematician(2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer

work page 1998

[20] [20]

Fokkinga, and Ross Paterson

Erik Meijer, Maarten M. Fokkinga, and Ross Paterson. 1991. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. InFunctional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings (Lecture Notes in Computer Science, Vol. 523), John Hughes (Ed.). Springer, 124–144. doi:10....

work page doi:10.1007/3540543961_7 1991

[21] [21]

Gerhard Osius. 1974. Categorical Set Theory: A Characterization of the Category of Sets.Journal of Pure and Applied Algebra4, 1 (Feb. 1974), 79–119. doi:10.1016/0022-4049(74)90032-2

work page doi:10.1016/0022-4049(74)90032-2 1974

[22] [22]

Podelski and A

A. Podelski and A. Rybalchenko. 2004. Transition invariants. InProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.32–41. doi:10.1109/LICS.2004.1319598

work page doi:10.1109/lics.2004.1319598 2004

[23] [23]

Intrinsic Verification of 22 Cass Alexandru, Henning Urbat, and Thorsten Wißmann Parsers and Formal Grammar Theory in Dependent Lambek Calculus

Steven Schaefer, Nathan Varner, Pedro Henrique Azevedo de Amorim, and Max S. New. 2025. Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus.Agda Formalization of "Intrinsic Verification of 22 Cass Alexandru, Henning Urbat, and Thorsten Wißmann Parsers and Formal Grammar Theory in Dependent Lambek Calculus"9, PLDI (June...

work page 2025

[24] [24]

Bonsangue, and Jan J

Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. 2013. Generalizing determinization from automata to coalgebras.Logical Methods in Computer Science9, 1 (2013). doi:10.2168/LMCS-9(1:9)2013

work page doi:10.2168/lmcs-9(1:9)2013 2013

[25] [25]

1999.Practical Foundations of Mathematics

Paul Taylor. 1999.Practical Foundations of Mathematics. Cambridge University Press. doi:10.2307/3621547

work page doi:10.2307/3621547 1999

[26] [26]

Henning Urbat and Thorsten Wißmann. 2025. Well-Founded Coalgebras Meet König’s Lemma. arXiv:2507.18539 [cs.LO] https://arxiv.org/abs/2507.18539 To appear in CSL 2026

work page arXiv 2025

[27] [27]

Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types.Proc. ACM Program. Lang.3, ICFP (July 2019), 87:1–87:29. doi:10.1145/3341691 Intrinsically Correct Algorithms and Recursive Coalgebras 23 A Preservation Properties for Recursive Coalgebras We present tw...

work page doi:10.1145/3341691 2019