A brief presentation of Coq

Some features of the Coq system are illustrated by the development of a certified program of insertion sort on lists of integers.
The source file is here (V8) .

You should notice that this development uses many tactics which are defined in the rest of the book. This example aims to give a flavour of coq programming, and you should focus on the global structure more than on technical details.
Nevertheless, as for any example in this site, it is a good practice to replay it on your computer, and even try to modify it.

Going home

Pierre Castéran