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 9721C7F79D for ; Mon, 18 Aug 2014 17:58:48 +0200 (CEST) X-IronPort-AV: E=Sophos;i="5.01,886,1400018400"; d="scan'208";a="89728868" Received: from yquem.inria.fr ([128.93.8.37]) by mail2-relais-roc.national.inria.fr with ESMTP; 18 Aug 2014 17:58:48 +0200 Received: by yquem.inria.fr (Postfix, from userid 18184) id 8452BE1A81; Mon, 18 Aug 2014 17:58:48 +0200 (CEST) Date: Mon, 18 Aug 2014 17:58:48 +0200 From: Hugo Herbelin To: caml-list@inria.fr Message-ID: <20140818155848.GA12519@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] 2nd CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call) 2nd call for papers: Types for Proofs and Programs, post-proceedings of TYPES 2014 (open call) ---------------------------------------------- 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: 1 September 2014 Paper submission deadline: 8 September 2014 Notification of acceptance: 15 February 2015 Details ------- * Papers must be submitted in PDF format using EasyChair: "https://www.easychair.org/conferences/?conf=types14postproceedings". * 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. Incidentally, publication of TYPES 2013 post-proceedings is imminent as volume 26 of the LIPIcs series Informatics. * 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. Editors ------- Hugo Herbelin Inria Paris-Rocquencourt, France Pierre Letouzey University Paris-Diderot, France Matthieu Sozeau Inria Paris-Rocquencourt, France