[isabelle] new AFP entry: Imperative Insertion Sort



"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.”

Many thanks to Christian Sternagel for this entry!

Larry Paulson






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.