Intrinsically Correct Algorithms and Recursive Coalgebras
summary
Presents a new sufficient criterion: functors on families indexed by a well-founded relation that factor through restriction are well-founded functors, and every coalgebra for such a functor is provably recursive coalgebra. Implements the proof and several case studies (Quicksort, Euclid GCD, CYK) and provides an Octa library with a Cubical Agda formalization, showing the approach produces terminating, intrinsically correct algorithms and reusable mechanized artifacts.
AI-written summary · about
chapters (13)
- 0:00Recursive coalgebras introduction
- 1:47Divide and conquer algorithms
- 3:56Morphisms in structured recursion
- 5:45Recursive coalgebras for termination
- 7:31Intrinsic correctness proofs
- 9:21Quicksort correctness indexing
- 11:10Wellfounded functors and proofs
- 13:22API for wellfoundedness proofs
- 14:30Quicksort wellfounded functor
- 16:37Conclusion and future work
- 17:22Q&A on functors
- 18:44Q&A on wellfounded orderings
- 19:48Q&A on CYK parsing
related talks
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq
27mIntrinsically Correct Sorting in Cubical Agda
29mIntroduction to Recursion Schemes
15mA systematic approach to "Well-founded recursion done right"
21mWell-founded recursion done right
58mCoalgebra for the working programming languages researcher
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
31mAbstract your representation and fix your functors