[TYPES/announce] An important 3 months event in 2014 and two close deadlines

[curien at pps.jussieu.fr]

In this message, we want to give a preliminary announcement about the
following event:

*****************************
IHP thematic trimester   (in Paris) 
(http://www.ihp.fr/en/activities/quarters/ceb)

"Semantics of proofs and certified mathematics"  (see below for an overall
description of the scope)

which will be held

from April 7 to July 11, 2014.

******************************

We shall very soon create a specific web page for this event (wait for the
second announcement!), with a preregistration interface.

All kinds of attendance are imaginable for these trimesters:

- attendance to a single workshop (see below for the list of the workshops
planned), or to a thematic course,
- longer stays, up to the whole duration of the trimester (a number of
offices are at the disposal of the participants),
- even longer stays (6 months or one/two years) including the period of
the trimester.

In particular, we want to draw the attention of potential applicants -- 
and  of colleagues who may have good ideas for encouraging applications --
on the following two programs (open to mathematical sciences in  the
large), with

*** rather short deadlines! ***


1) The annual postdoctoral programme of the Foundation "Sciences
Mathématiques de Paris", of which the organisers of the trimester are
members.

 ** Deadline 2 december 2012 **

(This programme offers  1 year or 2 years postdoctoral positions)

http://www.sciencesmaths-paris.fr/en/postdoctoral-programmes-247.htm

2)  A new joint programme of the IHP and IHES that is specially devoted to
supporting IHP trimesters:

** Deadline 12 december 2012 **

http://www.ihes.fr/jsp/site/Portal.jsp?document_id=2953&portlet_id=1043

(This programme offers  6 months visiting researcher positions and 1 years
postdoctoral positions)

Both programs are highly competitive, but highly worth trying!

If you intend to apply, or if you are determined to stay at least a month
during the trimester (there are various other schemes that we can use for
this)
please contact beforehand any of the organisers of the  IHP trimester:

Pierre-Louis Curien <curien at pps.univ-paris-diderot.fr>
Hugo Herbelin <hugo.herbelin at inria.fr>
Paul-Andre Mellies <mellies at pps.univ-paris-diderot.fr>



**********  SEMANTICS OF PROOFS AND CERTIFIED MATHEMATICS  ********

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.

Besides various courses, spontaneous working groups,  individual
collaborations, etc..., the programme will host
five thematic workshops:

** Formalization of mathematics in proof assistants

** Constructive mathematics and models of type theory

** Semantics of proofs and programs

** Abstraction and verification in semantics

** Certification of high-level and low-level programs}

***********************************