From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 19EF2820A1 for ; Wed, 4 Sep 2013 23:25:44 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of alx@mimuw.edu.pl) identity=pra; client-ip=193.0.96.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alx@mimuw.edu.pl"; x-sender="alx@mimuw.edu.pl"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of alx@mimuw.edu.pl) identity=mailfrom; client-ip=193.0.96.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alx@mimuw.edu.pl"; x-sender="alx@mimuw.edu.pl"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail.mimuw.edu.pl) identity=helo; client-ip=193.0.96.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alx@mimuw.edu.pl"; x-sender="postmaster@mail.mimuw.edu.pl"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjABAP2kJ1LBAGAGnGdsb2JhbABaDoMug3m/RBYOAQEBAQEIFAk8gk4PAQUwECoMAgUMBwMLAgsDAgECAUsNCAEBiAIImTGOf4k4iE6BKYs9gwuCX4E0A5d1lEdB X-IPAS-Result: AjABAP2kJ1LBAGAGnGdsb2JhbABaDoMug3m/RBYOAQEBAQEIFAk8gk4PAQUwECoMAgUMBwMLAgsDAgECAUsNCAEBiAIImTGOf4k4iE6BKYs9gwuCX4E0A5d1lEdB X-IronPort-AV: E=Sophos;i="4.90,1023,1371074400"; d="scan'208";a="31524064" Received: from mail.mimuw.edu.pl ([193.0.96.6]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 04 Sep 2013 23:25:42 +0200 Received: from localhost (localhost [127.0.0.1] ident=amavis) by duch.mimuw.edu.pl (Postfix) with ESMTP id 3417839; Wed, 4 Sep 2013 23:25:42 +0200 (CEST) X-Virus-Scanned: amavisd-new at mimuw.edu.pl Received: from duch.mimuw.edu.pl ([127.0.0.1]) by localhost (mail.mimuw.edu.pl [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id Zu9SQNktg7C3; Wed, 4 Sep 2013 23:25:36 +0200 (CEST) Received: from aronia.mimuw.edu.pl (unknown [46.31.32.17]) (using TLSv1 with cipher DHE-RSA-CAMELLIA256-SHA (256/256 bits)) (No client certificate requested) by duch.mimuw.edu.pl (Postfix) with ESMTPSA; Wed, 4 Sep 2013 23:25:32 +0200 (CEST) Message-ID: <5227A546.7060102@mimuw.edu.pl> Date: Wed, 04 Sep 2013 23:25:26 +0200 From: Aleksy Schubert User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130805 Thunderbird/17.0.8 MIME-Version: 1.0 To: Aleksy Schubert Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Subject: [Caml-list] Final CFP Post-proceedings TYPES 2013 Types for Proofs and Programs (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 2013, which was held in Toulouse, 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. - Formalisation of proofs in type theory. - Extraction of implementations from proofs. - Automation in computer-assisted reasoning. - Links between type theory and functional programming. - Links between type theory and object-oriented programming. - Type theory in linguistics. Important dates --------------- Abstract submission deadline: 2013-09-09 Paper submission deadline: 2013-09-16 Notification of acceptance: 2014-02-17 Details ------- * Papers must be submitted in PDF format using EasyChair: https://www.easychair.org/conferences/?conf=types13postproceedin * 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 together with the papers. * 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. * Authors of accepted papers retain copyright, but are expected to sign an author agreement with Schloss Dagstuhl—Leibniz-Zentrum für Informatik, see http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/. * For information about how to prepare submissions, see http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/. In general, please refer to the dedicated web site http://www.irit.fr/TYPES2013/Postproceedings.html for more detailed/specific information. * We recommend to keep the length of the contributions in the range of 15-25 pages. Editors ------- Ralph Matthes IRIT (CNRS and University of Toulouse), France Aleksy Schubert University of Warsaw, Poland