22 April 2014 – 11 July 2014
After years of steady development, the technology of proof assistants is currently coming to a mature state. As a matter of fact, it is possible today to formalize a non trivial mathematical proof inside a computer, and to check its correctness automatically. This "tour de force" has been recently achieved for the four color theorem, and a certified proof of the classification of finite groups and of the Kepler conjecture are on the way.
These achievements would not have been possible without the rich and active mathematics of formal proofs which emerged in the 1970s at the frontier of logic and computer science, along the Curry-Howard correspondence. This seminal correspondence enables us to understand a logical proof (of a given formula) as a well-behaved program (of a given type). Besides this by now traditional connection between logic and computer science, a number of unexpected connections are currently emerging with other fields of mathematics – this including homotopy theory, higher dimensional algebra, quantum topology, topos theory, functional analysis and operator algebra. Finally, proof assistants have been successfully applied to certify properties of programs written in high-level languages as well as low-level languages, to implement certified compilers, or to establish important security properties of protocols.
The purpose of this thematic trimester is to provide a forum for the extended community of researchers and students in mathematics and in computer science interested in proof assistants, and more generally, in the mathematics of formal proofs. Much care will be devoted during the trimester to train the mathematicians interested to learn and to use the current proof assistants in their work.
Expected to be held from April 7th to April 18th 2014.
From April 22th to July 11th 2014, the trimester will favour informal collaborations between participants. It will offer some courses (to be announced) and host five workshops, scheduled as follows:
| Week | Event | Subject | Organizers |
|---|---|---|---|
| 1 | Kick-off | Formalisation in mathematics and in computer science | |
| 3 | Workshop 1 | Formalization of mathematics in proof assistants | Georges Gonthier and Vladimir Voevodsky |
| 6 | Workshop 2 | Constructive mathematics and models of type theory | Thierry Coquand and Thomas Streicher |
| 8 | Workshop 3 | Semantics of proofs and programs | Thomas Ehrhard and Alex Simpson |
| 10 | Workshop 4 | Abstraction and verification in semantics | Paul-André Melliès and Luke Ong |
| 12 | Workshop 5 | Certification of high-level and low-level programs | Christine Paulin and Zhong Shao |
A five-weeks event on the Mathematical Structures of Computation is organised in Lyon, as a progamme of the Laboratoire d'Excellence MILYON, Together, the two programmes may be considered as a French Semester on certified mathematics, programming languages and the mathematical structures of computation.
Funding schemes of different kinds are available for financial support, or partial financial support. Requests will have to be made at registration time, and will be treated with an eye on equilibrium of themes, on eligibility for the different means that we have at our disposal, etc.
Preregistration is now closed. Thank you to all participants who have preregistered. This helped us to calibrate the overall organisation of the event.
The proper registration phase is now open. All future participants (preregistered or not) are now invited to visit IHP's website, to proceed to registration. Participants who wish to apply for some financial support have to register by September 16th, 2013.
Here is a list of people who have preregistered:
The Institut Henri Poincaré is located 11 Rue Pierre et Marie Curie, 75005 Paris France.
Contact the organizers: Pierre-Louis Curien, Hugo Herbelin, Paul-André Melliès.
For problems or suggestions concerning the website: Samuel Mimram.