[isabelle-dev] Merge-Sort Implementation

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 27 14:50:11 CEST 2011

Hi Christian,

> please find attached the formalization of the merge-sort algorithm as
> used in GHC's standard library. See also:
> http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort

interesting to read that comment.  The exiting quicksort implementation
in HOL is indeed taken from Isabelle's ML library.  Don't know what the
ancient motivation for quicksort has been (maybe others can comment on

A critical question: according to the comment, this should easily
generalize to a stable sort_key implementation (as also the current
quicksort does).  Have you undertaken this?

All the best,



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111027/5f7262eb/attachment.sig>

More information about the isabelle-dev mailing list