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 AFAA17EE63; Tue, 30 Apr 2013 12:24:57 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of curien@pps.univ-paris-diderot.fr) identity=pra; client-ip=194.254.61.138; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="curien@pps.univ-paris-diderot.fr"; x-sender="curien@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 curien@pps.univ-paris-diderot.fr) identity=mailfrom; client-ip=194.254.61.138; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="curien@pps.univ-paris-diderot.fr"; x-sender="curien@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="curien@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: AiUEAHWbf1HC/j2Kf2dsb2JhbAA8FoM9gl1aqm+QMYECFg4BAQsLCggUKIIyF0URGRwCDxcCSReILAiTSZsISoF2jl+BI4wtEgEFgRAigkOBEwOBNZcPimiGdIE7gWgBCBc X-IPAS-Result: AiUEAHWbf1HC/j2Kf2dsb2JhbAA8FoM9gl1aqm+QMYECFg4BAQsLCggUKIIyF0URGRwCDxcCSReILAiTSZsISoF2jl+BI4wtEgEFgRAigkOBEwOBNZcPimiGdIE7gWgBCBc X-IronPort-AV: E=Sophos;i="4.87,580,1363129200"; d="scan'208";a="12735260" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 30 Apr 2013 12:24:32 +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/38117) with ESMTP id r3UAOWTJ016896; Tue, 30 Apr 2013 12:24:32 +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 239D24C087; Tue, 30 Apr 2013 12:24:32 +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 10024) with ESMTP id Wkck7sm-nnRW; Tue, 30 Apr 2013 12:24:28 +0200 (CEST) Received: from webmail.math.univ-paris-diderot.fr (webmail.math.univ-paris-diderot.fr [81.194.30.252]) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTP id 035574C086; Tue, 30 Apr 2013 12:24:27 +0200 (CEST) User-Agent: SOGoMail 2.0.2 cc: curien@pps.univ-paris-diderot.fr X-Forward: 89.93.195.44 MIME-Version: 1.0 from: "Pierre-Louis Curien" message-id: <4067-517f9c00-f-52caf080@4416057> to: coq-club@inria.fr, caml-list@inria.fr content-type: text/plain; charset="utf-8" date: Tue, 30 Apr 2013 12:24:27 +0200 content-transfer-encoding: quoted-printable X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (korolev.univ-paris7.fr [194.254.61.138]); Tue, 30 Apr 2013 12:24:32 +0200 (CEST) X-Validation-by: curien@pps.univ-paris-diderot.fr Subject: [Caml-list] Thematic trimester "Semantics of proofs and certified mathematics", spring 2014, Paris We are pleased to announce the following important event. A 3-months trimester "Semantics of proofs and certified mathematics" will take place at the Institut Henri Poincar=C3=A9, Paris, France in the spring 2014 (from 22 April to 11 July, preceded by a preschool at CI= RM, Marseille). Details are enclosed below. Pierre-Louis Curien, Hugo Herbelin, and Paul-Andr=C3=A9 Melli=C3=A8s (organ= isers) ********************** Dear colleague, It is our pleasure to announce a programme on "Semantics of proofs and cert= ified mathematics" organised by the Centre Emile Borel of Henri Poincare In= stitute in Paris, from April 7th to July 11th, 2014. The organisers are Pierre-Louis Curien, Hugo Herbelin and Paul-Andre Mellie= s. Information on the programme can be found at : http://www.ihp.fr/en or at h= ttp://ihp2014.pps.univ-paris-diderot.fr/ Registration for the programme is free and recommended on: http://www.ihp.f= r/en/program/10226/register BE CAREFUL : Deadline to apply for financial support is September 16th, 2013 During this trimester: - A summerschool 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: http://www.ihp.fr/en/program/10225/conference/register The number of participants to CIRM Summer School being limited, if necessar= y a selection among the applications will have to be made by the organisers. and - 5 workshops will take place: 1) =C2=AB Formalization of mathematics in proof assistants =C2=BB - May 5th= to 9th (except Thursday, 8th- bank holiday) 2) =C2=AB Constructive mathematics and models of type theory =C2=BB - June = 2th to 6th 3) =C2=AB Semantics of proofs and programs =C2=BB June 10th to 14th (Tuesda= y through Saturday- Monday, 9th-bank holiday) 4) =C2=AB Abstraction and verification in semantics =C2=BB June 23rd to 27th 5) =C2=AB Certification of high-level and low-level programs =C2=BB July 7t= h to 11th If you intend to participate to one or several of these events please regis= ter first to the whole programme. Registrations for these workshops will be= opened later on. I will at that time send you a message informing you about it. We are looking forward to welcoming you in Paris! The poster of the trimester programme may be retrieved from the site http:= //ihp2014.pps.univ-paris-diderot.fr/ PS: do not hesitate to forward this e-mail to your colleagues and students. Sorry for multiple e-mails reception. -- Claire B=C3=A9renger CEB Program Coordinator Institut Henri Poincare 11 rue Pierre et Marie Curie 75005 Paris FRANCE Tel: 01 44 27 67 64 Fax: 01 44 07 09 37 **************************************** Chers Coll=C3=A8gues, Nous avons le plaisir de vous annoncer l'organisation d'un programme sur la= "S=C3=A9mantique des preuves et des programmes et formalisation des math= =C3=A9matiques" au Centre Emile Borel (CEB) de l Institut Henri Poincar=C3= =A9 de Paris, du 7 avril au 11 juillet 2014. Les organisateurs sont: Pierre-Louis Curien, Hugo Herbelin et Paul-Andre Me= llies. Vous pouvez consulter le programme =C3=A0 l'adresse suivante: http://www.ih= p.fr/fr ou directement =C3=A0 cette adresse: http://ihp2014.pps.univ-paris-= diderot.fr/ L'inscription au programme est gratuite et cependant recommand=C3=A9e sur l= a page suivante: http://www.ihp.fr/fr/program/10225/register Attention : la date limite pour les demandes de support financier est fix=C3=A9e au 16 = septembre 2013. Durant ce trimestre: - une =C3=A9cole d =C3=A9t=C3=A9 est organis=C3=A9e au CIRM (Marseille) du = 7 au 18 avril 2014. Si vous avez l'intention de participer =C3=A0 ce programme en particulier u= ne pr=C3=A9-inscription est n=C3=A9cessaire sur le site suivant: http://www.ihp.fr/fr/program/10225/conference/register Le nombre de participants =C3=A0 l'=C3=A9cole d'=C3=A9t=C3=A9 du CIRM etant= limit=C3=A9, si necessaire une selection au vu des candidatures sera faite= par les organisateurs scientifiques. et - 5 conferences auront lieu: 1) =C2=AB Formalization of mathematics in proof assistants =C2=BB - du 5 au= 9 mai (=C3=A0 l exception du jeudi 8 mai- jour f=C3=A9ri=C3=A9) 2) =C2=AB Constructive mathematics and models of type theory =C2=BB - du 2 = au 6 juin 3) =C2=AB Semantics of proofs and programs =C2=BB June 10th to 14th (du mar= di au samedi- Lundi 9 - jour f=C3=A9ri=C3=A9) 4) =C2=AB Abstraction and verification in semantics =C2=BB du 23 au 27 juin 5) =C2=AB Certification of high-level and low-level programs =C2=BB du 7 au= 11 juillet Si vous avez l'intention de participer =C3=A0 une ou plusieurs de ces conf= =C3=A9rences merci de vous inscrire dans un premier temps au programme dans= son ensemble. Les conf=C3=A9rences seront ouvertes aux inscriptions ult=C3=A9rieurement. = Je vous en informerai par courriel. C'est avec plaisir que nous vous accueillerons a Paris! L'affiche du programme du trimestre est t=C3=A9l=C3=A9chargeable depuis le = site http://ihp2014.pps.univ-paris-diderot.fr/. PS: merci par avance de bien vouloir transmettre ce courriel =C3=A0 vos col= l=C3=A8gues et =C3=A9tudiants.