A Type-Based Approach to Divide-and-Conquer Recursion in Coq
summary
Presents a type-level interface that encodes divide-and-conquer recursion as Mendler-style algebras, implemented in Coq and expressible in System F_omega plus positive-recursive types. Key pieces are an abstract_in constructor and an SFO combinator to initiate subsidiary recursions; typing alone enforces termination so no dependent or size indices are required. Implements mergesort, quicksort, Harper’s continuation-based regex matcher and run-length encoding, and proves properties like sortedness and decode using an indexed induction variant.
AI-written summary · about
chapters (4)
related talks
29mIntroduction to Recursion Schemes
21mIntrinsically Correct Algorithms and Recursive Coalgebras
56mAn introduction to recursion schemes
31mAbstract your representation and fix your functors
30mConvenient Algebraic Programming with Coercive Subtyping
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
25mFulls Seldom Differ
34mPeeling the Banana: Recursion Schemes from First Principles