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 CDD567F722 for ; Thu, 17 Apr 2014 09:25:36 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.97,877,1389740400"; d="scan'208";a="68664436" Received: from yquem.inria.fr ([128.93.8.37]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Apr 2014 09:25:36 +0200 Received: by yquem.inria.fr (Postfix, from userid 18184) id C3BF2E1A42; Thu, 17 Apr 2014 09:25:36 +0200 (CEST) Date: Thu, 17 Apr 2014 09:25:36 +0200 From: Hugo Herbelin To: caml-list@inria.fr Message-ID: <20140417072536.GA15976@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: 2nd call for participation Types Meeting 2014 Paris, 12-15 May 2014 http://www.pps.univ-paris-diderot.fr/types2014 2nd 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 and 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, 39 contributed talks have been 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 only until ** April 19 **.