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@pps.univ-paris-diderot.fr> Hugo Herbelin <hugo.herbelin@inria.fr> Paul-Andre Mellies <mellies@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} *********************************** [For admin and other information see: http://www.mta.ca/~cat-dist/ ]