Result: Intrinsically Correct Sorting in Cubical Agda
Title:
Intrinsically Correct Sorting in Cubical Agda
Contributors:
Choudhury, Vikraman, Stark, K.
Source:
Stark, K. (ed.), CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs Denver CO USA January 20-21, 2025, pp. 34-49
Publication Status:
Preprint
Publisher Information:
ACM, 2025.
Publication Year:
2025
Subject Terms:
[MATH.MATH-CO] Mathematics [math]/Combinatorics [math.CO], Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Software Science, Mathematics - Combinatorics, F.3.2, Mathematics - Category Theory, F.3.1, [MATH.MATH-CT] Mathematics [math]/Category Theory [math.CT]
Document Type:
Academic journal
Article<br />Conference object
File Description:
application/pdf
DOI:
10.1145/3703595.3705873
Access URL:
Rights:
CC BY
Accession Number:
edsair.doi.dedup.....8fb6f4c05d7e88c63f20a39766364d8f
Database:
OpenAIRE
Further Information
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.