Lambda the Ultimate

The following article describes a verified version of the insertion sort algorithm. The insertion sort is one of the simplest sorting algorithms and efficient for small data sets.

In the article it is shown how ghost functions/predicates can be used to keep the loop invariant expressive and readable.