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.
Spring School in Theoretical Computer Science, 2015 edition
This spring school is meant for researchers in theoretical computer science who want to better understand what a proof assistant is and how to integrate its usage in their daily research work. Therefore, no prior knowledge about the domain of mechanized proofs is needed to attend this school. .
The school will be divided into eight sessions (09:30AM - 12:30PM and 14:00PM - 17:30PM). A session will consist in a (rather short) talk followed by practical exercises on computer.
Pedagogical documents and software will be made available on a USB stick provided on your arrival.
The five first sessions will be dedicated to a presentation of the main concepts and techniques used to mechanize proofs on a computer. We will especially study how to use inductive reasoning to prove algorithms and their realizations as functional and imperative programs.
The two next sessions will focus on the mechanization of two classic domains of theoretical computer science: the theory of rational languages and the computational combinatorics.
Finally, during the last session, participants will work on the mechanization of their specific research domain with the help of the pedagogical team of the school.
|Morning||Reasoning using Coq||Pierre Letouzey|
|Afternoon||Programming in Coq||Pierre Letouzey|
|Morning||Proof of functional programs||Matthieu Sozeau|
|Afternoon||Proof of imperative programs||Arthur Charguéraud|
|Morning||Mechanized mathematics for computer science||Assia Mahboubi|
|Morning||Mechanizing rational languages||Damien Pous|
|Afternoon||Proof by computation applied to some combinatorial problems||Benjamin Grégoire|
|Morning||Your research in Coq|
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.
Your accomodation includes a night on Sunday. Therefore, you can plan your arrival at the Saint Raphael train station on Sunday evening. We will arrange a bus around 20.00 to get you to the Villa Clythia. If you cannot take this bus for some reasons, please contact Yann Regis-Gianas as soon as possible so that we can organize car travels as well.
The school ends on Friday morning at 12.30PM. We will also have a bus from the Villa to the station around 14.00. Again, contact Yann Regis-Gianas if this does not work for you.
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)...
The school is sponsored by
- GDR Informatique Mathématique
- Fédération d'informatique fondamentale de Paris Diderot (LIAFA - PPS)