From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id CEA087F720 for ; Wed, 16 Apr 2014 10:11:58 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mellies@pps.univ-paris-diderot.fr) identity=pra; client-ip=194.254.61.138; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mellies@pps.univ-paris-diderot.fr"; x-sender="mellies@pps.univ-paris-diderot.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mellies@pps.univ-paris-diderot.fr) identity=mailfrom; client-ip=194.254.61.138; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mellies@pps.univ-paris-diderot.fr"; x-sender="mellies@pps.univ-paris-diderot.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@korolev.univ-paris7.fr) identity=helo; client-ip=194.254.61.138; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mellies@pps.univ-paris-diderot.fr"; x-sender="postmaster@korolev.univ-paris7.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmcBAOk6TlPC/j2KnGdsb2JhbAA/FgSDQbxJhzaBHhYOAQEBAQEICwkJFCiEdod8BAk2lCqyDBeOEQEBETqCOQ9ngRQElHaKQo8kgXA X-IPAS-Result: AmcBAOk6TlPC/j2KnGdsb2JhbAA/FgSDQbxJhzaBHhYOAQEBAQEICwkJFCiEdod8BAk2lCqyDBeOEQEBETqCOQ9ngRQElHaKQo8kgXA X-IronPort-AV: E=Sophos;i="4.97,870,1389740400"; d="scan'208,217";a="68467663" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 16 Apr 2014 10:11:58 +0200 Received: from mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [81.194.30.253]) by korolev.univ-paris7.fr (8.14.4/8.14.4/relay1/46573) with ESMTP id s3G8BvPa011600 for ; Wed, 16 Apr 2014 10:11:57 +0200 Received: from mailhub.math.univ-paris-diderot.fr (localhost [127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTP id AE58E135AE for ; Wed, 16 Apr 2014 10:11:57 +0200 (CEST) X-Virus-Scanned: amavisd-new at math.univ-paris-diderot.fr Received: from mailhub.math.univ-paris-diderot.fr ([127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [127.0.0.1]) (amavisd-new, port 10023) with ESMTP id tzhPXihXnOLS for ; Wed, 16 Apr 2014 10:11:56 +0200 (CEST) Received: from [134.157.87.241] (unknown [134.157.87.241]) (Authenticated sender: mellies) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id F28FA135A9 for ; Wed, 16 Apr 2014 10:11:55 +0200 (CEST) From: Paul-Andre Mellies Content-Type: multipart/alternative; boundary="Apple-Mail=_DE8F7CEA-58D5-4639-A877-9B30EF69A084" Message-Id: <2D361929-066C-47EF-904D-B15A95F713FF@pps.univ-paris-diderot.fr> Date: Wed, 16 Apr 2014 10:11:56 +0200 To: caml-list@yquem.inria.fr Mime-Version: 1.0 (Mac OS X Mail 7.2 \(1874\)) X-Mailer: Apple Mail (2.1874) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (korolev.univ-paris7.fr [194.254.61.138]); Wed, 16 Apr 2014 10:11:57 +0200 (CEST) X-Miltered: at korolev with ID 534E3B4D.000 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 534E3B4D.000 from mailhub.math.univ-paris-diderot.fr/mailhub.math.univ-paris-diderot.fr/null/mailhub.math.univ-paris-diderot.fr/ X-j-chkmail-Score: MSGID : 534E3B4D.000 on korolev.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Status: Ham X-Validation-by: mellies@pps.univ-paris-diderot.fr Subject: [Caml-list] IHP thematic trimester -- Kick-off meeting -- Tuesday April 22 --Apple-Mail=_DE8F7CEA-58D5-4639-A877-9B30EF69A084 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=windows-1252 Dear all, We are glad to announce the kick-off meeting of the thematic trimester=20 ** Semantics of proofs and certified mathematics ** which will be held at Institut Henri Poincar=E9 (IHP), Paris, on the aftern= oon of Tuesday, April 22, 2014. Four keynote speakers are invited to give a talk on this occasion: =95 Georges Gonthier (Microsoft Research, Cambridge, and Microsoft INRIA Jo= int Center, Palaiseau) Digitizing the Group Theory of the Odd Order Theorem =95 Thomas Hales (University of Pittsburgh) Formalizing the proof of the Kepler Conjecture =95 Xavier Leroy (INRIA Paris-Rocquencourt) Proof assistants in computer science research =95 Vladimir Voevodsky (Institute for Advanced Study, Princeton) Univalent Foundations - new type-theoretic foundations of mathematics More information on the thematic trimester will be found on the webpage https://ihp2014.pps.univ-paris-diderot.fr/doku.php You will find preliminary lists of confirmed invited speakers for the 5 wor= kshops of the IHP programme 5=969 May Workshop 1 Formalization of mathematics in proof assistan= ts=09=20 2=966 June Workshop 2 Constructive mathematics and models of type t= heory=09 10=9614 June Workshop 3 Semantics of proofs and programs=09 23=9627 June Workshop 4 Abstraction and verification in semantics=09 7=9611 July Workshop 5 Certification of high-level and low-level pr= ograms Registration to individual workshops is free but mandatory here: http://www.ihp.fr/en/ceb/trimester/proofs (you do not need to register to the trimester unless you intend to stay for= longer than the duration of a workshop) https://webmail.pps.univ-paris-diderot.fr/SOGo/so/curien/Mail/0/folderDraft= s/newDraft1384694494-1/edit# The organisers Pierre-Louis Curien Hugo Herbelin Paul-Andre Mellies --Apple-Mail=_DE8F7CEA-58D5-4639-A877-9B30EF69A084 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=windows-1252

De= ar all,

We are glad to announce the kick= -off meeting of the thematic trimester 
** Semantics of pro= ofs and certified mathematics **
which will be held at Institut= Henri Poincar=E9 (IHP), Paris, on the afternoon of Tuesday, April = 22, 2014.

Four keynote speakers are invited to give a talk on th= is occasion:

=95 Georges Gonthier (Micro= soft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau)
Digitizing the Group Theory of the Odd Order Theorem
=95&nb= sp;Thomas Hales (University of Pittsburgh)
Formalizin= g the proof of the Kepler Conjecture
=95 Xavier Leroy (= INRIA Paris-Rocquencourt)
Proof assistants in computer science re= search
=95 Vladimir Voevodsky (Institute for Adv= anced Study, Princeton)
<= div>2=966 June <= /span>        Workshop 2 Constructive mathem= atics and models of type theory
10=9614 June Workshop 3 Semantics of proofs and programs
23=9627 June Workshop 4= Abstract= ion and verification in semantics
7=9611 July        &= nbsp;Workshop 5 = Certification of high-level and low-level programs

Registrati= on to individual workshops is free but mandatory here:
http://www.ihp.fr/en/ceb/trimester/pro= ofs
(you do not need to register to the trimester unless you intend = to stay for longer than the duration of a workshop)
https://webmail.pps.univ-paris-diderot.fr/SOGo/so/curi= en/Mail/0/folderDrafts/newDraft1384694494-1/edit#

The organisers=
Pierre-Louis Curien <curien@pps.univ-paris-diderot.fr>
Hugo Herbelin <Hugo.Herbelin@inria.fr>
Paul-A= ndre Mellies <melli= es@pps.univ-paris-diderot.fr>

= --Apple-Mail=_DE8F7CEA-58D5-4639-A877-9B30EF69A084--