# 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. [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. BibTeX: @article{Efficient-Mergesort-AFP, 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: Regex_Equivalence Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.