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