Abstract

We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art proof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.

BibTeX

@article{CS-JAR12,
  author      = "Christian Sternagel",
  title       = "Proof Pearl - A Mechanized Proof of GHC's Mergesort",
  journal     = "Journal of Automated Reasoning",
  volume      = 51,
  number      = 4,
  pages       = "357--370",
  year        = 2012
}