# Imperative Insertion Sort

 Title: Imperative Insertion Sort Author: Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) Submission date: 2014-09-25 Abstract: The insertion sort algorithm of Cormen et al. (Introduction to Algorithms) is expressed in Imperative HOL and proved to be correct and terminating. For this purpose we also provide a theory about imperative loop constructs with accompanying induction/invariant rules for proving partial and total correctness. Furthermore, the formalized algorithm is fit for code generation. BibTeX: @article{Imperative_Insertion_Sort-AFP, author = {Christian Sternagel}, title = {Imperative Insertion Sort}, journal = {Archive of Formal Proofs}, month = sep, year = 2014, note = {\url{https://isa-afp.org/entries/Imperative_Insertion_Sort.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License 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.