Email Gateway (Aug 19 2022 at 15:55): Email Gateway (Aug 19 2022 at 15:55):From: Lawrence Paulson <lp15@cam.ac.uk>
"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
Last updated: Apr 26 2024 at 20:16 UTC