Efficient Mergesort

Christian Sternagel

9 November 2011

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.
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

Topics

Theories

Cite

×
@article{Efficient-Mergesort-AFP,
  author  = {Christian Sternagel},
  title   = {Efficient Mergesort},
  journal = {Archive of Formal Proofs},
  month   = November,
  year    = 2011,
  note    = {\url{http://isa-afp.org/entries/Efficient-Mergesort.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download