Efficient Mergesort

Christian Sternagel

9 November 2011


We provide a formalization of the mergesort algorithm as used in GHC's Data.List module, proving correctness and stability. Furthermore, experimental data suggests that generated (Haskell-)code for this algorithm is much faster than for previous algorithms available in the Isabelle distribution.
BSD License

Change history

[2012-10-24] Added reference to journal article.
[2018-09-17] Added theory Efficient_Mergesort that works exclusively with the mutual induction schemas generated by the function package.
[2018-09-19] Added theory Mergesort_Complexity that proves an upper bound on the number of comparisons that are required by mergesort.
[2018-09-19] Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old name Efficient_Sort. [2020-11-20] Additional theory Natural_Mergesort that developes an efficient mergesort algorithm without key-functions for educational purposes.

Used by