Binary Heaps for IMP2

Title:	Binary Heaps for IMP2
Author:	Simon Griebel
Submission date:	2019-06-13
Abstract:	In this submission array-based binary minimum heaps are formalized. The correctness of the following heap operations is proved: insert, get-min, delete-min and make-heap. These are then used to verify an in-place heapsort. The formalization is based on IMP2, an imperative program verification framework implemented in Isabelle/HOL. The verified heap functions are iterative versions of the partly recursive functions found in "Algorithms and Data Structures – The Basic Toolbox" by K. Mehlhorn and P. Sanders and "Introduction to Algorithms" by T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein.
BibTeX:	@article{IMP2_Binary_Heap-AFP, author = {Simon Griebel}, title = {Binary Heaps for IMP2}, journal = {Archive of Formal Proofs}, month = jun, year = 2019, note = {\url{https://isa-afp.org/entries/IMP2_Binary_Heap.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	IMP2
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.