×

Proof pearl: A mechanized proof of GHC’s mergesort. (English) Zbl 1314.68288

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

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68P10 Searching and sorting
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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 · Zbl 1214.68335
[2] 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 · Zbl 1284.68131
[3] 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 · Zbl 1214.68335 · doi:10.1007/s10817-009-9157-2
[4] 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 · Zbl 0994.68131
[5] O’Keefe, R.: A smooth applicative merge sort. Tech. rep., Department of Artificial Intelligence, University of Edinburgh (1982)
[6] Paulson, L.C.: ML for the Working Programmer, 2nd edn. Cambridge University Press, New York (1996) · Zbl 0863.68032 · doi:10.1017/CBO9780511811326
[7] 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)
[8] 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 · Zbl 1252.68265
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.