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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 819297F790 for ; Thu, 24 Apr 2014 19:54:45 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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: At8IABNPWVPC/j2KW2dsb2JhbABZgmUhT70dh3WBHRYDGAsKBxMqg0SBBS2IQQEDCZktsiYTBI5VIYMOgRUEn1SPMQ X-IPAS-Result: At8IABNPWVPC/j2KW2dsb2JhbABZgmUhT70dh3WBHRYDGAsKBxMqg0SBBS2IQQEDCZktsiYTBI5VIYMOgRUEn1SPMQ X-IronPort-AV: E=Sophos;i="4.97,920,1389740400"; d="scan'208,217";a="58800452" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail3-smtp-sop.national.inria.fr with ESMTP; 24 Apr 2014 19:54:44 +0200 Received: from potemkin.univ-paris7.fr (potemkin.univ-paris7.fr [IPv6:2001:660:3301:8000::1:1]) by korolev.univ-paris7.fr (8.14.4/8.14.4/relay1/46573) with ESMTP id s3OHsif4020383 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO) for ; Thu, 24 Apr 2014 19:54:44 +0200 Received: from mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [81.194.30.253]) by potemkin.univ-paris7.fr (8.14.4/8.14.4/relay2/46573) with ESMTP id s3OHsiv0015353 for ; Thu, 24 Apr 2014 19:54:44 +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 795B814D28 for ; Thu, 24 Apr 2014 19:54:44 +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 N0tMsdVDfcTd for ; Thu, 24 Apr 2014 19:54:43 +0200 (CEST) Received: from [134.157.87.249] (unknown [134.157.87.249]) (Authenticated sender: mellies) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id E90AE14D24 for ; Thu, 24 Apr 2014 19:54:42 +0200 (CEST) From: Paul-Andre Mellies Content-Type: multipart/alternative; boundary="Apple-Mail=_74AE6841-E17D-4237-A3B5-C14F9FB27012" Message-Id: <2535F5D7-30B2-47D7-A2CD-3431FDA86931@pps.univ-paris-diderot.fr> Date: Thu, 24 Apr 2014 19:54:46 +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 [IPv6:2001:660:3301:8000::1:2]); Thu, 24 Apr 2014 19:54:44 +0200 (CEST) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (potemkin.univ-paris7.fr [194.254.61.141]); Thu, 24 Apr 2014 19:54:44 +0200 (CEST) X-Miltered: at korolev with ID 53594FE4.001 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-Miltered: at potemkin with ID 53594FE4.000 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 53594FE4.001 from potemkin.univ-paris7.fr/potemkin.univ-paris7.fr/null/potemkin.univ-paris7.fr/ X-j-chkmail-Enveloppe: 53594FE4.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 : 53594FE4.001 on korolev.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Score: MSGID : 53594FE4.000 on potemkin.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Status: Ham X-j-chkmail-Status: Ham X-Validation-by: mellies@pps.univ-paris-diderot.fr Subject: [Caml-list] thematic trimester at IHP -- talks of the first week available online --Apple-Mail=_74AE6841-E17D-4237-A3B5-C14F9FB27012 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=iso-8859-1 Dear colleagues, We are happy to announce that the lectures of the first week of the themati= c trimester=20 =AB Semantics of Proofs and Certified Mathematics =BB=20 are available online on the channel of the Institut Henri Poincar=E9: https://www.youtube.com/watch?v=3DONs_6TPe1bE&list=3DPL9kd4mpdvWcCUOrG5S7Kr= vOFDhyqnXoUj Besides the keynote talks given during the kick-off meeting of the trimeste= r: Georges GONTHIER (Microsoft Research, Cambridge, and MSR-INRIA Joint Centre= , Palaiseau) Thomas HALES (University of Pittsburgh) Xavier LEROY (INRIA Paris - Rocquencourt) Vladimir VOEVODSKY (Institute for Advanced Study, Princeton) two mini-courses of three hours each by=20 G=E9rard BERRY (Coll=E8ge de France) Jean-Yves GIRARD (CNRS, Institut de Math=E9matiques de Luminy) Hope that you enjoy the recordings, The organizers, Pierre-Louis Curien Hugo Herbelin Paul-Andr=E9 Melli=E8s = --Apple-Mail=_74AE6841-E17D-4237-A3B5-C14F9FB27012 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=iso-8859-1
Dear colleagues,

We are happy to announce that the lectures of the= first week of the thematic trimester 
=AB Semantics= of Proofs and Certified Mathematics =BB 
are avail= able online on the channel of the Institut Henri Poincar=E9:

=

Besides the keynote talks given during the kick-off m= eeting of the trimester:

Georges GONTHIER (Microsoft= Research, Cambridge, and MSR-INRIA Joint Centre, Palaiseau)
Thomas H= ALES =         (University of Pittsburgh)<= br>Xavier LEROY         (INRIA Paris - Rocquencourt)=
Vladimir VOEVODSKY (Institute for Advanced Study, Princeton)
two mini-courses of three hours each by 

G=E9rard BERRY (Coll=E8ge de France)
<= b>Jean-Yves GIRARD (CNRS, Institut de Math=E9matiques de Lumi= ny)

Hope that you enjoy the recordings,

The organizers,

Pierre-L= ouis Curien <curien@pps.univ-paris-diderot.fr>
Hugo H= erbelin <h= erbelin@inria.fr>
Paul-Andr=E9 Melli=E8s <mellies@pp= s.univ-paris-diderot.fr>
= --Apple-Mail=_74AE6841-E17D-4237-A3B5-C14F9FB27012--