Journal ArticleOPEN ACCESS

Proof pearl - A mechanized proof of GHC's mergesort

Journal of Automated Reasoning (2013) 51(4) 357-370
DOI: 10.1007/s10817-012-9260-7
10Citations
Citations of this article
10Readers
Mendeley users who have this article in their library.

This article is free to access.

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. © 2012 The Author(s).

Author supplied keywords

Cite

CITATION STYLE

APA

Sternagel, C. (2013). Proof pearl - A mechanized proof of GHC’s mergesort. Journal of Automated Reasoning, 51(4), 357–370. https://doi.org/10.1007/s10817-012-9260-7

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free