From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7882 Path: news.gmane.org!not-for-mail From: Hugo Herbelin Newsgroups: gmane.science.mathematics.categories Subject: "Semantics of proofs and certified mathematics", IHP trimester, Paris, spring 2014: call for starting school application and workshop registration Date: Wed, 9 Oct 2013 18:52:43 +0200 Message-ID: Reply-To: Hugo Herbelin NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1381458053 12603 80.91.229.3 (11 Oct 2013 02:20:53 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 11 Oct 2013 02:20:53 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Fri Oct 11 04:20:56 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1VUSLY-0003k1-1Z for gsmc-categories@m.gmane.org; Fri, 11 Oct 2013 04:20:56 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:36554) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1VUSJ1-0007kj-VJ; Thu, 10 Oct 2013 23:18:19 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1VUSJ2-0003wS-K2 for categories-list@mlist.mta.ca; Thu, 10 Oct 2013 23:18:20 -0300 Content-Disposition: inline Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7882 Archived-At: Semantics of proofs and certified mathematics --------------------------------------------- special programme organised by the Centre ?mile Borel of Henri Poincar? Institute Paris, April 7th - July 11th, 2014 http://www.ihp.fr/en/ceb/trimester/proofs http://ihp2014.pps.univ-paris-diderot.fr/ Application for starting school at CIRM (Marseille) and registration for workshops at IHP (Paris) is open (registration for workshops is necessary for logistical reasons). If you intend to attend the school or one or several workshops, please register also to the full trimester. * Workshops * Kick-off: Formalisation in mathematics and in computer science May 5-9: Formalization of mathematics in proof assistants Organisers: Georges Gonthier and Vladimir Voevodsky June 2-6: Constructive mathematics and models of type theory Organisers: Thierry Coquand and Thomas Streicher June 10-14: Semantics of proofs and programs Organisers: Thomas Ehrhard and Alex Simpson June 23-27: Abstraction and verification in semantics Organisers: Luke Ong and Igor Walukiewicz July 7-11: Certification of high-level and low-level programs Organisers: Christine Paulin and Zhong Shao * Starting school lecturers * April 7-11: Thierry Coquand, Assia Mahboubi, Alexandre Miquel April 14-18: Amal Ahmed, Pierre-Louis Curien, Alex Simpson * Associated events hosted at IHP * May 12-16: TYPES conference + Proof, Computation, Complexity workshop May 26-30: Mathematics, Algorithms, Proofs conference (MAP) The call for participation for these events will be announced separately by the respective organisers. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]