Formalization of an insertion sort in Coq and Why3

We model an insertion sort and prove it correct, in Coq and in Why3.

Insertion sort on lists in Coq

The Coq source can be found here. It has been tested with Coq 8.6.1.

Insertion sort on arrays in Why3

The archive can be found here. It has been tested with the development version of Why3. The exact versions of Why3 and of the provers can be found in the archive.