cl-banner

Proof Pearl - A Mechanized Proof of GHC's Mergesort

Christian Sternagel

Journal of Automated Reasoning 51(4), pp. 357 – 370, 2012.

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.

 

  PDF |    doi:10.1007/s10817-012-9260-7  |  © 2012, Springer Science + Business Media B.V. (Open Access)

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
}
Nach oben scrollen