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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Filliâtre, J.C., Magaud, N.: Certification of sorting algorithms in the Coq system. In: Theorem Proving in Higher Order Logics: Emerging Trends (1999). http://www-sop.inria.fr/croap/TPHOLs99/proceeding.html
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming, FLOPS 2010, Lecture Notes in Computer Science, vol. 6009, pp. 103–117. Springer (2010). doi:10.1007/978-3-642-12251-4_9
Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reasoning 44(4), 303–336 (2010). doi:10.1007/s10817-009-9157-2
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a proof assistant for higher-order logic. In: Lecture Notes in Computer Science, vol. 2283. Springer (2002). doi:10.1007/3-540-45949-9
O’Keefe, R.: A smooth applicative merge sort. Tech. rep., Department of Artificial Intelligence, University of Edinburgh (1982)
Paulson, L.C.: ML for the Working Programmer, 2nd edn. Cambridge University Press, New York (1996)
Sternagel, C.: Efficient Mergesort. In: Klein, G., Nipkow, T., Paulson, L.C. (eds.) The Archive of Formal Proofs. http://afp.sf.net/entries/Efficient-Mergesort.shtml (2011, formal proof development)
Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, TPHOLs 2009, Lecture Notes in Computer Science, vol. 5674, pp. 452–468. Springer (2009). doi:10.1007/978-3-642-03359-9_31
Author information
Authors and Affiliations
Corresponding author
Additional information
This research is supported by the Austrian Science Fund (FWF): J3202.
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 2.0 International License (https://creativecommons.org/licenses/by/2.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
About this article
Cite this article
Sternagel, C. Proof Pearl—A Mechanized Proof of GHC’s Mergesort. J Autom Reasoning 51, 357–370 (2013). https://doi.org/10.1007/s10817-012-9260-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-012-9260-7