A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free

on YouTube ↗26m

" summary

Proves that a mergesort implementation satisfying a specific characteristic property yields correctness (sorted + permutation) and stability, for many variants: top-down, bottom-up, tail-recursive, non-tail, smooth and non-smooth, and even library versions for Okl and Huskell. Uses relational parametricity and an automated parametricity translation to produce witnesses, formalized in the Rocq Prover. Deduces an induction-on-traces principle and a naturality/free-theorem; fails only for a GHC merge that uses four lists.

AI-written summary · about

" chapters (16)

1. 0:00Parametricity and mergesort proofs
2. 1:02Mergesort correctness paper
3. 2:24Top-down vs bottom-up mergesort
4. 4:18Mergesort characteristic property
5. 7:14Parametricity and abstraction theorem
6. 9:03Relational parametricity explained
7. 11:11Induction from characteristic property
8. 14:49Naturality of mergesort
9. 17:23Tail-recursive and smooth mergesort
10. 18:28GHC mergesort challenges
11. 18:50Conclusion and implications
12. 19:36Q&A: Stability and characteristic property
13. 21:02Q&A: Instantiation and type constraints
14. 22:24Q&A: Generality and specific theorems
15. 23:28Q&A: Applicability to other sorts
16. 23:50Q&A: Formalization and axioms