### Context: Why should we verify proofs?

Ensuring reproducibility is an important aspect of the scientific method. Contrary to one may think, purely theoretical domains, like mathematics and theoretical computer science, do not avoid this problem in practice even though the reproducibility of a proof only requires reasoning principles, which are a priori independent of the experimental conditions. Indeed, proofs in modern mathematics and in theoretical computer science are so complex that it is hard to honestly claim that they are perfectly valid. These proofs are so large and they are based on so many concepts that a manual verification of the validity of every details is extremely difficult. Besides, the devil is in the details : an unsound lemma may jeopardize a large number of derived results by a domino effect.

Proof assistants are software in charge of verifying every single reasoning step in a proof. Since several years, there is a growing interest in these tools. In that context, Vladimir Voevodsky, who won the Fields medal, launched an ambitious research program about the foundations of mathematics that gives a central role to the usage of a proof assistant to mechanically build correct-by-construction proofs. The Coq proof assistant has been chosen by Voevodsky as a basis for this project.

In computer science too, software are known to reach a level of complexity that overcomes our ability to manually check the correctness of programs with respect to their specifications. The famous "bugs" come from mistakes in the implementation of programs. Since the 60s, we know that programs enjoy a deep connection with mathematical proofs, the so-called Curry-Howard correspondence , and that one can devise proof systems that ensure that programs are correct-by-construction. The Coq proof assistant provides such a proof system by means of a very expressive type system. As a tool to prove programs, Coq has been distinguished by the prestigious Software System Award of the Association for Computing Machinery.

At the frontier between computer science and mathematics, theoretical computer science produces complex mathematical reasoning about its objects of study (the algorithm, the computational complexity, the cryptographic methods, the formal languages, ...). Theoretical computer scientists are also interested in a concrete realization of these objects by a computer. From the perspective of the reproducibility of scientific results, the challenge of the theoretical computer scientist is twofold: on the one hand, he must ensure the absence of errors in his mathematical proofs and on the other hand, he must ensure that his programs are faithful realizations of the mathematical objects they are supposed to represent.

Currently, several domains of theoretical computer science (proof theory, programming language theory, verification of cryptographic protocols, ...) already have recognized the benefits of using a proof assistant in formal developments. In other domains, even the exact nature of this tool is unknown.

The main objective of this spring school is to introduce the Coq proof assistant to researchers from the very beginning, and especially to researchers from domains of theoretical computer science that are not using proof assistants yet.

### Program

Monday 05/25 | ||

Morning | Reasoning using Coq | Pierre Letouzey |

Afternoon | Programming in Coq | Pierre Letouzey |

Tuesday 05/26 | ||

Morning | Proof of functional programs | Matthieu Sozeau |

Afternoon | Proof of imperative programs | Arthur Charguéraud |

Wednesday 05/27 | ||

Morning | Mechanized mathematics for computer science | Assia Mahboubi |

Afternoon | Break | |

Thursday 05/28 | ||

Morning | Mechanizing rational languages | Damien Pous |

Afternoon | Proof by computation applied to some combinatorial problems | Benjamin Grégoire |

Friday 05/29 | ||

Morning | Your research in Coq |

### Registration

To register to this spring school, please follow this link.

Registration deadline: 2015/04/30

Full pension in a room for two: 375 euros.

Full pension in a room for one: 440 euros.

### Localization

This school will take place in Fréjus (France) in the villa Clythia.

To relax between two Coq proofs:

- a swimming pool,
- a large forest, the see, beautiful landscapes,
- sport facilities (volley, tennis, basket)...