Intrinsically Correct Sorting in Cubical Agda

This conference talk from CPP 2025 explores how to implement intrinsically correct sorting algorithms using Cubical Agda. Learn how researchers Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide extend the work from "Sorting with Bialgebras and Distributive Laws" by Hinze et al. to create formally verified sorting implementations. Discover their innovative approach of indexing data types by multisets to guarantee that sorting algorithms terminate with ordered permutations of input lists. The presentation demonstrates how lifting bialgebraic semantics to the indexed setting allows deriving correctness proofs directly from distributive laws between functors. The 27-minute talk covers sorting algorithm pairs like insertion/selection sort and quick/tree sort, showing how both folds and unfolds can be used in their construction. Access the full paper and supplementary artifacts to explore the implementation details in Cubical Agda.