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 674067EFCB; Thu, 20 Feb 2014 10:38:13 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of matthieu.sozeau@gmail.com) identity=pra; client-ip=74.125.82.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="matthieu.sozeau@gmail.com"; x-sender="matthieu.sozeau@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of matthieu.sozeau@gmail.com designates 74.125.82.174 as permitted sender) identity=mailfrom; client-ip=74.125.82.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="matthieu.sozeau@gmail.com"; x-sender="matthieu.sozeau@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f174.google.com) identity=helo; client-ip=74.125.82.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="matthieu.sozeau@gmail.com"; x-sender="postmaster@mail-we0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At0BAP/LBVNKfVKulWdsb2JhbABZDoMwg1m+FRYOAQEBAQcNCQkSKoJJBh0BJxIDDQUfAiYCNgEFASIBiAMDEQQBCKEcjAtOgxOVOycNh3ARAQUMgR2MY4MODzE1gRQEmDCBMoUViXBBgWWCNUCBZw X-IPAS-Result: At0BAP/LBVNKfVKulWdsb2JhbABZDoMwg1m+FRYOAQEBAQcNCQkSKoJJBh0BJxIDDQUfAiYCNgEFASIBiAMDEQQBCKEcjAtOgxOVOycNh3ARAQUMgR2MY4MODzE1gRQEmDCBMoUViXBBgWWCNUCBZw X-IronPort-AV: E=Sophos;i="4.97,511,1389740400"; d="scan'208";a="49769321" Received: from mail-we0-f174.google.com ([74.125.82.174]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 20 Feb 2014 10:38:12 +0100 Received: by mail-we0-f174.google.com with SMTP id w61so1245804wes.19 for ; Thu, 20 Feb 2014 01:38:12 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:from:content-type:content-transfer-encoding:subject :message-id:date:to:mime-version; bh=tM43f09ZxBdUiT5PrFhaWqKdR0NDYl5xzJ3zP/JLrUk=; b=EbD28RXGTk2IkOCNpPJLUEjgioyy/wzsvUxrBMQMBQldGmKtYJTlxhhi+sdcfeUCvm x2/Qb6LcrcU89zblyuR32OExgo9+NN4Oaou9B556GqdPObDPlOxMMsPdfBldJGa6paD9 tOMELqtwyzMyyd2EGBjfWPXmmolLzI9oA9c9EMU6UMTnzscxKTXKEe5CiEVjM0TxhWcg RcjB+AkxIOg+KWsSXXkr/VI6RsQGye7+5DPVjcsg9G/nGPw0F2OR83kjGWW6Q/JOOXTa B0r1z9LlWKvzq6Ta7HWJ++GbTKKouL5g7PTXsyWQUqY1SsBi5jQ2eNcoNhq7lRrcBSx4 xseQ== X-Received: by 10.194.23.201 with SMTP id o9mr839588wjf.67.1392889092119; Thu, 20 Feb 2014 01:38:12 -0800 (PST) Received: from [192.168.1.30] ([78.193.5.8]) by mx.google.com with ESMTPSA id n15sm9773996wij.3.2014.02.20.01.38.09 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Thu, 20 Feb 2014 01:38:10 -0800 (PST) Sender: Matthieu Sozeau From: Matthieu Sozeau Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Message-Id: <8FBFA09F-E978-4B76-9F4A-8975478F57BF@inria.fr> Date: Thu, 20 Feb 2014 10:38:21 +0100 To: types@lists.chalmers.se, types-announce@lists.seas.upenn.edu, Coq Club , Agda mailing list , homotopytypetheory , Isabelle users , matita@cs.unibo.it, twelf-list@itu.dk, mizar-forum@mizar.uwb.edu.pl, gdr-im@gdr-im.fr, haskell@haskell.org, caml-list@inria.fr Mime-Version: 1.0 (Mac OS X Mail 7.1 \(1827\)) X-Mailer: Apple Mail (2.1827) X-Validation-by: mattam@mattam.org Subject: [Caml-list] TYPES 2014 in Paris, May 12 - 15: last call for contributions TYPES Meeting 2014 Paris, 12-15 May 2014 http://www.pps.univ-paris-diderot.fr/types2014/ LAST CALL FOR CONTRIBUTIONS The 20th Conference "Types for Proofs and Programs" will take place in Paris, France, from 12 to 15 May 2014. 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. Invited speakers: * Thierry Coquand * Xavier Leroy * Andy Pitts We invite all researchers to contribute talks on subjects related to the Types area of interest. These include, but are not limited to: * Foundations of type theory and constructive mathematics; * Homotopy type theory; * Applications of type theory; * Dependently typed programming; * Industrial uses of type theory technology; * Meta-theoretic studies of type systems; * Proof assistants and proof technology; * Automation in computer-assisted reasoning; * Links between type theory and functional programming; * Formalizing mathematics using type theory. We would like to especially encourage talks proposing new ways of applying type theory. The talks may be based on newly published papers, work submitted for publication, but also work in progress. There are no formal pre-proceedings, but we will make available the abstract book for the conference. TYPES has post-proceedings which will be announced in a separate call for papers. Participation in TYPES 2014 is no prerequisite for submission to the post-proceedings. TYPES 2014 is intended to be a conference in our traditional workshop style. We expect submission of short abstracts that fit on one or two pages, presenting in sufficient detail the content of the talk and its relevance for TYPES, as judged by the program committee. Submission for a contributed talk consists in a short LaTeX abstract in EasyChair style that fits on one or two pages to be included in the abstract book. The submission site is https://www.easychair.org/conferences/?conf=3Dtypes2014 . Please announce your intention to submit an abstract by first submitting a title one week in advance. Dates: * title: Friday February 21 (midnight GMT) * submission of short abstracts: Friday February 28 (midnight GMT) * notification of acceptance: Monday March 17 * final version of short abstracts: Friday April 11 The conference will be held at the Institut Henri Poincar=C3=A9 in the 5th district of Paris. It will happen on week 4 of the special trimester on Semantics of proofs and certified mathematics (see http://ihp2014.pps.univ-paris-diderot.fr). Satellite event: the 13th international workshop Proof, Computation,=20 Complexity (PCC 2014) will be held on May 15th and 16th. Program Committee: * Andreas Abel, Chalmers University of Technology and Gothenburg University * Andrej Bauer, Fakulteta za matematiko in fiziko, Ljubljana * Ma=C5=82gorzata Biernacka, University of Wroclaw * Lars Birkedal, Aarhus University * Paul Blain Levy, University of Birmingham * Herman Geuvers, Radboud University and Eindhoven University of Technology * Hugo Herbelin, Inria Paris-Rocquencourt (co-chair) * Pierre Letouzey, University Paris-Diderot (co-chair) * Ralph Matthes, IRIT, CNRS and University of Toulouse * Conor McBride, University of Strathclyde * Lu=C3=ADs Pinto, University of Minho, Braga * Claudio Sacerdoti, University of Bologna * Aleksy Schubert, University of Warsaw * Matthieu Sozeau, Inria Paris-Rocquencourt (co-chair) * Thomas Streicher, TU Darmstadt=