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 6209A7FACC for ; Fri, 29 Aug 2014 17:37:49 +0200 (CEST) X-IronPort-AV: E=Sophos;i="5.04,425,1406584800"; d="scan'208";a="92098301" Received: from yquem.inria.fr ([128.93.8.37]) by mail2-relais-roc.national.inria.fr with ESMTP; 29 Aug 2014 17:37:49 +0200 Received: by yquem.inria.fr (Postfix, from userid 18184) id 4E43F2062; Fri, 29 Aug 2014 17:37:49 +0200 (CEST) Date: Fri, 29 Aug 2014 17:37:49 +0200 From: Hugo Herbelin To: caml-list@inria.fr Message-ID: <20140829153749.GA14327@yquem.inria.fr> Mail-Followup-To: caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) Subject: [Caml-list] Final CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call, extended deadline) Final call for papers: Types for Proofs and Programs, post-proceedings of TYPES 2014 (open call) (with deadline extension and corrected submission link) ------------------------------------------------- TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. The post-proceedings of TYPES 2014, which was held May 12-15 in Paris, are open to everyone, also those who did not participate in the conference. We would like to invite all researchers that study type systems to share their results concerning type-based theorem proving environments or type-based formal modelling, in particular we welcome submissions on any topic in the following list: - Foundations of type theory and constructive mathematics - 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 - Formalising mathematics using type theory. Important dates --------------- Abstract submission deadline: 8 September 2014 (new deadline) Paper submission deadline: 15 September 2014 (new deadline) Notification of acceptance: 15 February 2015 Details ------- * Papers must be submitted in PDF format using EasyChair: "https://www.easychair.org/conferences/?conf=types14postproceedin". * Authors have the option to include an attachment (.zip or .tgz) containing mechanised proofs, but reviewers are not obliged to take these attachments into account. Attachments will not be published. * The post-proceedings will be published in LIPIcs (Leibniz International Proceedings in Informatics, "http://www.dagstuhl.de/en/publications/lipics"), an open-access series of conference proceedings (TYPES 2013 post-proceedings have been published last July as volume 26 of the LIPIcs series Informatics, see http://drops.dagstuhl.de/portals/extern/index.php?semnr=14006). * We recommend to keep the length of the contributions in the range of 15-25 pages, and 25 pages is the upper limit for the submissions. More detailed instructions are given at "https://www.pps.univ-paris-diderot.fr/types2014/PostProceedings". Editors ------- Hugo Herbelin Inria Paris-Rocquencourt, France Pierre Letouzey University Paris-Diderot, France Matthieu Sozeau Inria Paris-Rocquencourt, France