Efficient Mergesort


Title: Efficient Mergesort
Author: Christian Sternagel
Submission date: 2011-11-09
Abstract: 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.
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.
  author  = {Christian Sternagel},
  title   = {Efficient Mergesort},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2011,
  note    = {\url{https://isa-afp.org/entries/Efficient-Mergesort.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Used by: Berlekamp_Zassenhaus, Regex_Equivalence