Back to Search Start Over

Proof Pearl—A Mechanized Proof of GHC’s Mergesort.

Authors :
Sternagel, Christian
Source :
Journal of Automated Reasoning; Dec2013, Vol. 51 Issue 4, p357-370, 14p
Publication Year :
2013

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. [ABSTRACT FROM AUTHOR]

Subjects

Subjects :
AUTOMATIC theorem proving
SORTING (Electronic computers)
ALGORITHMS
COMPUTER software correctness
STABILITY theory
CODING theory

Details

Language :
English
ISSN :
01687433
Volume :
51
Issue :
4
Database :
Complementary Index
Journal :
Journal of Automated Reasoning
Publication Type :
Academic Journal
Accession number :
91996867
Full Text :
https://doi.org/10.1007/s10817-012-9260-7
Full Text Access
View/download PDF

Tools

Authors Abstract Subjects Details