Efficient Mergesort

 

Title: Efficient Mergesort
Author: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
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
BibTeX:
@article{Efficient-Mergesort-AFP,
  author  = {Christian Sternagel},
  title   = {Efficient Mergesort},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2011,
  note    = {\url{http://isa-afp.org/entries/Efficient-Mergesort.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Used by: Berlekamp_Zassenhaus, Regex_Equivalence