Intrinsically Correct Sorting in Cubical Agda

Abstract

The paper “Sorting with Bialgebras and Distributive Laws” by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.

Citation

BibTeX citation:

@inproceedings{alexandru2025,
  author = {Alexandru, Cass and Choudhury, Vikraman and Rot, Jurriaan
    and van der Weide, Niels},
  title = {Intrinsically {Correct} {Sorting} in {Cubical} {Agda}},
  booktitle = {Certified Programs and Proofs},
  date = {2025},
  url = {https://doi.org/10.1145/3703595.3705873},
  doi = {10.1145/3703595.3705873},
  langid = {en},
  abstract = {The paper “Sorting with Bialgebras and Distributive Laws”
    by Hinze et al. uses the framework of bialgebraic semantics to
    define sorting algorithms. From distributive laws between functors
    they construct pairs of sorting algorithms using both folds and
    unfolds. Pairs of sorting algorithms arising this way include
    insertion/selection sort and quick/tree sort. We extend this work to
    define intrinsically correct variants in cubical Agda. Our key idea
    is to index our data types by multisets, which concisely captures
    that a sorting algorithm terminates with an ordered permutation of
    its input list. By lifting bialgebraic semantics to the indexed
    setting, we obtain the correctness of sorting algorithms purely from
    the distributive law.}
}

For attribution, please cite this work as:

Alexandru, Cass, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide. 2025. “Intrinsically Correct Sorting in Cubical Agda.” Certified Programs and Proofs, accepted. https://doi.org/10.1145/3703595.3705873.