Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

This is an old revision of the document!


Semantics of proofs and certified mathematics

Institut Henri Poincaré thematic trimester

Presentation

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.

Programme

Pre-school at the CIRM

A spring school at CIRM is organized from April 7th to April 18th, 2014: If you intend to participate in this event, it will be necessary to make a pre-registration through this link. The number of participants to CIRM Spring School being limited, if necessary a selection among the applications will have to be made by the organisers.

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 April – 1 MayLecturesFrançois Pottier, Thorsten Altenkirch and Jean-Louis Krivine
5–9 May Workshop 1 Formalization of mathematics in proof assistants
12–16 MayTYPES 2014
19–20 MayJournéesJournées de la Fédération de recherche en mathématiques de Paris-Centre
21–23 MayLectures
26–30 MayMAP 2014
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 JuneLectures
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
  • A five-weeks event on the Mathematical Structures of Computation is 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.
  • The TYPES 2014 conference will be held at IHP on week 4, 12-15 May, followed by the Proof, Computation, Complexity workshop.
  • 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.

Registration

Registration is now open (and free). All future participants are invited to

  1. and then register to the individual workshops
    (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.

Location

The Institut Henri Poincaré is located 11 Rue Pierre et Marie Curie, 75005 Paris France.

Sponsors

Contacts

Contact the organizers: Pierre-Louis Curien, Hugo Herbelin, Paul-André Melliès.

For problems or suggestions concerning the website: Samuel Mimram.

start.1394636608.txt.gz · Last modified: 2014/03/12 16:03 by smimram
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