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.
A spring school at CIRM is organized from April 7th to April 18th, 2014. Submission for funding is not possible anymore, but a few rooms are still available.
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:
|22 April||Kickoff||Georges Gonthier, Thomas Hales, Xavier Leroy and Vladimir Voevodsky|
|23–25 April||Lectures||Gérard Berry and Jean-Yves Girard|
|28 April||Industry||Formal methods for reliable software development in industry|
|28–30 April||Lectures||Thorsten Altenkirch, Jean-Louis Krivine, Per Martin-Löf and François Pottier|
|5–9 May||Workshop 1||Formalization of mathematics in proof assistants|
|12–16 May||TYPES 2014||TYPES conference|
|19–21 May||Journées||Journées de la Fédération de recherche en mathématiques de Paris-Centre|
|22–28 May||AIM XIX||19th Agda Implementor's Meeting|
|26–28 May||Lectures||Timothy Gowers and Bruno Valette|
|26–30 May||MAP 2014||Mathematics, Algorithms, Proofs conference|
|2–6 June||Workshop 2||Constructive mathematics and models of type theory|
|10–14 June||Workshop 3||Semantics of proofs and programs|
|16–18 June||Workshop||Higher order computation: types, complexity, applications|
|16–20 June||Lectures||Martin Hyland, Marc Pouzet, Olivier Serre and Thomas Streicher|
|23–27 June||Workshop 4||Abstraction and verification in semantics|
|30 June–4 July||Lectures|
|7–11 July||Workshop 5||Certification of high-level and low-level programs|
Registration is open and free. It is requested for logistic reasons. All participants are invited to
Submission for funding is not possible anymore.
The Institut Henri Poincaré is located 11 Rue Pierre et Marie Curie, 75005 Paris France.