Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Semantics of proofs and certified mathematics

Institut Henri Poincaré thematic trimester


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.


Pre-school at the CIRM

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.

IHP Trimester

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:

Dates Event Theme
22 AprilKickoffGeorges Gonthier, Thomas Hales, Xavier Leroy and Vladimir Voevodsky
23–25 AprilLecturesGérard Berry and Jean-Yves Girard
28 AprilIndustryFormal methods for reliable software development in industry
28–30 AprilLecturesThorsten 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 MayTYPES 2014TYPES conference
19–21 MayJournéesJournées de la Fédération de recherche en mathématiques de Paris-Centre
22–28 MayAIM XIX19th Agda Implementor's Meeting
26–28 MayLecturesTimothy Gowers and Bruno Valette
26–30 MayMAP 2014Mathematics, 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 JuneWorkshopHigher order computation: types, complexity, applications
16–20 JuneLecturesMartin Hyland, Marc Pouzet, Olivier Serre and Thomas Streicher
23–27 June Workshop 4 Abstraction and verification in semantics
30 June–4 JulyLectures
7–11 July Workshop 5 Certification of high-level and low-level programs
  • The TYPES 2014 conference was held at IHP on week 4, 12-15 May, followed by the Proof, Computation, Complexity workshop.
  • The XIX-th Agda Implementors' Meeting is being held on weeks 5 and 6, 22-28 May.
  • A special edition on constructive mathematics of the MAP 2014 conference (Mathematics, Algorithms and Proofs) will be held at IHP on week 6, 26-30 May.
  • Bourbaki seminar on Saturday 21 June with talks by Thierry Coquand et Thomas Hales.
  • A five-weeks event on the Mathematical Structures of Computation was organised in Lyon from January 13th to February 14th, 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.


Registration is open and free. It is requested for logistic reasons. All participants are invited to

  1. visit IHP's website to register for the general event, mentioning the dates of presence (kick-off, industry afternoon, lectures, workshops 1 to 5)
  2. workshops 1 to 5 need an extra specific registration (please register first to the whole programme above if you intend to participate to one or several of the workshops)

Submission for funding is not possible anymore.


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.

start.txt · Last modified: 2014/05/28 09:30 by mellies
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0