# 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.