Title: 
 Certification of Sorting Algorithms in the Coq System 
   J.-C. Filliatre and N. Magaud

Speaker:
   Nicolas Magaud

Abstract:
We present the formal proofs of total correctness of three sorting algorithms 
in the Coq system, namely insertion sort, quicksort and heapsort.
The implementations are imperative programs working in-place on a given array.
Those developments demonstrate the usefulness of inductive types and 
higher-order logic in the process of software certification. 
They also show that the proof of rather complex algorithms may be done 
in a small amount of time - only a few days for each development - 
and without great difficulty.