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 18B037F89F for ; Wed, 26 Mar 2014 11:11:37 +0100 (CET) X-IronPort-AV: E=Sophos;i="4.97,734,1389740400"; d="scan'208";a="64803934" Received: from yquem.inria.fr ([128.93.8.37]) by mail2-relais-roc.national.inria.fr with ESMTP; 26 Mar 2014 11:11:37 +0100 Received: by yquem.inria.fr (Postfix, from userid 18184) id 0D277E1976; Wed, 26 Mar 2014 11:11:37 +0100 (CET) Date: Wed, 26 Mar 2014 11:11:37 +0100 From: Hugo Herbelin To: caml-list@inria.fr Message-ID: <20140326101137.GA18277@yquem.inria.fr> Mail-Followup-To: caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit User-Agent: Mutt/1.5.21 (2010-09-15) Subject: [Caml-list] Types Meeting 2014 in Paris, 12 - 15 May: call for participation Types Meeting 2014 Paris, 12-15 May 2014 http://www.pps.univ-paris-diderot.fr/types2014 CALL FOR PARTICIPATION The 20th Conference "Types for Proofs and Programs" will take place at the Institut Henri Poincaré (IHP) in Paris, France, from 12 to 15 May 2014, continued by the post-conference workshop "Proof, Computation, Complexity" overlapping TYPES on May 15 afternoon and on May 16. Types is this year an event associated to the special IHP trimester on Semantics of proofs and certified mathematics (https://ihp2014.pps.univ-paris-diderot.fr). Invited speakers are * Thierry Coquand, University of Gothenburg, Sweden A cubical set model of type theory * Xavier Leroy, INRIA Paris-Rocquencourt, France Formal verification of a static analyzer: abstract interpretation in type theory * Andy Pitts, University of Cambridge, UK Nominal sets in dependent type theory The Types Meeting is a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalized and computer assisted reasoning and computer programming. It works as a conference in our traditional workshop style and, this year, close to 40 contributed talks are in the process of being selected by the program committee on the basis of abstracts of up to two pages (see http://www.pps.univ-paris-diderot.fr/types2014/Program). Registration is open, with early rate until April 19.