Intrinsically Correct Sorting in Cubical Agda
summary
Claims intrinsic correctness of bialgebraic sorting follows solely from a distributive law lifted to an indexed setting; implementation uses Cubical Agda with quotient inductive types and path constructors to define a finite multiset index that enforces element preservation, orderedness, and gives a termination measure for unfolds. Verifies insertion/bubble, quick/tree and bottom-up/top-down heap variants; correctness reduces to a small non-recursive business logic. Artifacts and code are available (DOI 10.1145/3703595.3705873; Zenodo archive).
AI-written summary · about
chapters (10)
- 0:00Intrinsically correct sorting
- 2:30Motivation and paper
- 5:58Categorical semantics
- 8:28Bi-algebraic semantics
- 11:21Intrinsically correct base functors
- 13:10Indexing lists by multisets
- 14:54Termination via well-foundedness
- 18:32Distributive law in indexed setting
- 20:42Summary and future work
- 22:47Q&A
related talks
21mIntrinsically Correct Algorithms and Recursive Coalgebras
30mThe conatural numbers form an exponential commutative semiring
29mRepresenting Data Structures with Invariants in Haskell: the cases of BST and AVL
17mComputing with Generic Trees in Agda
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
30mConvenient Algebraic Programming with Coercive Subtyping
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq