The objective of this school is to teach the use of the Coq proof assistant that has received the SIGPLAN Programming Languages Software 2013 Award and the 2013 ACM Software System Award. It will consist of lectures and practices in English by internationally renowned experts in Coq.

Prerequisites. No previous knowledge of Coq will be necessary to follow the lectures. Students are however requested to attend the school with their own computer with the latest stable version of Coq and one of its user interfaces (CoqIDE ? distributed with Coq, or Proof General) installed. They are freely available online:
・ Coq and CoqIDE: http://coq.inria.fr
・ Proof General: http://proofgeneral.inf.ed.ac.uk

What is the Coq proof assistant? In principle, all mathematics can be formalized in axiomatic set theory, and then checked automatically by a computer. In the last century, more practical foundations for mathematics, based on type theory, have been designed and implemented as proof assistants. One of the most prominent is Coq, developed in France since 1984. They can check proofs and organize them in searchable libraries. They also provide convenient interfaces that help the user make proofs incrementally, and fill in automatically the trivial parts.

What can be done with Coq? In the beginning, proof assistants could only be used to formalize toy examples. It is however not anymore the case. Proof assistants have reached maturity and can deal with difficult mathematical results. For example, in December 2004, Gonthier has announced the full formalization of the four colors theorem in the Coq proof assistant (cf. Notices of the AMS 55(11), 2008). A more recent example is the proof of the Feit-Thompson theorem completed in Coq in 2012.

Mathematicians are not the only ones to make mathematical proofs. Computer scientists, for instance, make their own proofs. In a software, a small error can indeed result in serious damages in terms of safety and security. It is thus important to provide formal proofs that a software is correct: extensive testing of software or hardware is not enough because it may still miss errors that would be avoided with the use of a proof assistant. One prominent example is the formalization of a complete Java Card system in the Coq proof assistant and the certification that it meets the highest security requirements for industrial product, i.e., the Common Criteria EAL7 level. This was achieved in 2003 by Trusted Logic, a company that provides secure software for smart cards, terminals and consumer devices. Another example is the compiler Compcert: it is proved in Coq that it will always generate assembly code that has the same semantics than the source code in C. From the mathematician’s eye, some of those proofs may not appear difficult but they are nonetheless tricky and error-prone because they involve huge formal objects such as programs or automata, or require to consider hundreds of cases.