Master Class - "Coq, formal proof management system"

The Coq system provides a simplified programming language for describing algorithms, the logical properties of these algorithms, and proofs that the logical properties are satisfied. The key feature of this language is an enhanced version of typing as found in conventional programming languages. Although simplified, this language is powerful enough to describe advanced software, such as a Java virtual machine, a C compiler or a microprocessor.

What will I discover in this master class?

In this master class we will use the database example to show how to apply Coq to model operations on data sets (intersection, union, selection). Logical properties illustrate how different sequences of operations can lead to the same result. The proof techniques focus on the basic logical connectors and on the technique that allows reasoning about sets of unlimited size: recursive proof.

A research director at Inria, Yves Bertot specializes in type-theoretic proofs, successively studying the properties of programming languages, algorithmic geometry, mathematical computations and the interactions between formal proofs and formal algebraic computations. He is co-author with Pierre Castéran of the first book on the Coq system, "Interactive Theorem Proving And Program Development, Coq'art: The Calculus Of Inductive Constructions", published in 2004. He has contributed to some of the most remarkable results obtained with the Coq system, such as the CompCert compiler and the computer proof of the odd-order theorem.