From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10043 Path: news.gmane.org!.POSTED.blaine.gmane.org!not-for-mail From: Marc.Bezem@uib.no Newsgroups: gmane.science.mathematics.logic.coq.club,gmane.comp.lang.agda,gmane.science.mathematics.categories,gmane.comp.science.types.announce Subject: Final CfP: TYPES 2019 post-proceedings, deadline 24.11 Date: Wed, 13 Nov 2019 10:13:16 +0100 Message-ID: <20191113101316.29846kv3mt9to6r0.nmimb@impmail.uib.no> Reply-To: coq-club@inria.fr Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; DelSp="Yes"; format="flowed" Content-Transfer-Encoding: 7bit Injection-Info: blaine.gmane.org; posting-host="blaine.gmane.org:195.159.176.226"; logging-data="16636"; mail-complaints-to="usenet@blaine.gmane.org" User-Agent: Internet Messaging Program (IMP) H3 (4.3.9) Cc: Assia Mahboubi To: eutypes@cs.ru.nl, coq-club@inria.fr, agda@lists.chalmers.se, categories@mta.ca, types-announce@lists.seas.upenn.edu Original-X-From: coq-club-owner@inria.fr Wed Nov 13 11:05:23 2019 Return-path: Envelope-to: gsmlcc-coq-club@gmane.org Original-Received: from mail2-relais-roc.national.inria.fr ([192.134.164.83]) by blaine.gmane.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.89) (envelope-from ) id 1iUpWc-00047L-Cr for gsmlcc-coq-club@gmane.org; Wed, 13 Nov 2019 11:05:22 +0100 X-IronPort-AV: E=Sophos;i="5.68,300,1569276000"; d="scan'208";a="411562379" Original-Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 13 Nov 2019 11:05:20 +0100 Original-Received: by sympa.inria.fr (Postfix, from userid 20132) id 9CF197F32D; Wed, 13 Nov 2019 11:05:20 +0100 (CET) Original-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 25C8F7F30F for ; Wed, 13 Nov 2019 10:13:21 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Marc.Bezem@uib.no; spf=None smtp.mailfrom=nmimb@webmail.uib.no; spf=None smtp.helo=postmaster@alfons.uib.no IronPort-PHdr: =?us-ascii?q?9a23=3AXdCGSBFV70VbpnsXhhi3Op1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ7ypMiwAkXT6L1XgUPTWs2DsrQY0rGQ6vu5EjRZqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba58IRmssAncuNQajYR+Jqos1xDEvmZGd+?= =?us-ascii?q?NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLD?= =?us-ascii?q?TRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljj?= =?us-ascii?q?oMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2z?= =?us-ascii?q?cpEPAvIBM+hGsofyqEcBogaxCwaiH+7v1j1FimPq0aEmyektDAfL1xEgEdIUt3?= =?us-ascii?q?TUqc34OqAIXuCv0KbE1yjOYO1X2Djj7YjFaQ0hofCXUr5qd8rRzk8iHB7LgFWX?= =?us-ascii?q?rIzqJTKV1uIVvmeG9eVgWvmvi3I6qwFxpjij3NojhZfRio0L0F/E7iV4z5o1Jd?= =?us-ascii?q?KiSU57e8SoEJxKtyGVMYZ9X8AsQ3lwtSon1LELvYS3cDUIxZkl3RLSZeCLf5KV?= =?us-ascii?q?7h/sSeqdOTN1iGx/dL X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CFAQBAyMtdh40esYFlDg4BAQEBAQcBA?= =?us-ascii?q?REBBAQBAYF+gUuBQYEHKgqNIqFagXABAwEMJQcBAgEBg3uCZRwGBjQTAg4BAQQ?= =?us-ascii?q?BAQECAQIDBAETAQEBCgsJCBsOhT4MgjspAYMQIwEBJhEBR3cSgyIBgncBAwEKs?= =?us-ascii?q?DmCfgEBBYFLD4RHgSkJgTaJT4JFgheEYYEEflULAQMYgQIfZYUvjRSJQZdEB4l?= =?us-ascii?q?CjiQnjhyLYo5HiDaRbgMBgWWBejODRQEBMglHERRXkEMMDAuEA4Q+I4UEPEIxY?= =?us-ascii?q?yIBAY1egj8BAQ?= X-IPAS-Result: =?us-ascii?q?A0CFAQBAyMtdh40esYFlDg4BAQEBAQcBAREBBAQBAYF+gUu?= =?us-ascii?q?BQYEHKgqNIqFagXABAwEMJQcBAgEBg3uCZRwGBjQTAg4BAQQBAQECAQIDBAETA?= =?us-ascii?q?QEBCgsJCBsOhT4MgjspAYMQIwEBJhEBR3cSgyIBgncBAwEKsDmCfgEBBYFLD4R?= =?us-ascii?q?HgSkJgTaJT4JFgheEYYEEflULAQMYgQIfZYUvjRSJQZdEB4lCjiQnjhyLYo5Hi?= =?us-ascii?q?DaRbgMBgWWBejODRQEBMglHERRXkEMMDAuEA4Q+I4UEPEIxYyIBAY1egj8BAQ?= X-IronPort-AV: E=Sophos;i="5.68,299,1569276000"; d="scan'208";a="411548811" X-MGA-submission: =?us-ascii?q?MDErYbaOAxECrspNlBu0v/tKrFHf2EfALPAzVh?= =?us-ascii?q?VvJZSKFTH+T+cd1vPVLqh+gO8YoCU65WRDK5r5gK9ikNWQy2kNXSZAv/?= =?us-ascii?q?EPa+k8cAITuYRL9bryBXPBcDqFh3QQy5RRp4dZO3ZcnEIxGttWXg2IFm?= =?us-ascii?q?GJKKt4UkVZIj9G+VplXiIfFQ=3D=3D?= Original-Received: from alfons.uib.no ([129.177.30.141]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 13 Nov 2019 10:13:20 +0100 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=uib.no; s=20160927; h=Content-Transfer-Encoding:Content-Type:MIME-Version:Subject:Cc: To:From:Date:Message-ID:Sender:Reply-To:Content-ID:Content-Description: Resent-Date:Resent-From:Resent-Sender:Resent-To:Resent-Cc:Resent-Message-ID: In-Reply-To:References:List-Id:List-Help:List-Unsubscribe:List-Subscribe: List-Post:List-Owner:List-Archive; bh=G2guVbnUtx6mBFoINEB0ns7RH5aN8RtF5vZtYqI1YiA=; b=D/8pap9gO37/DSR809DdwmedBB VS8hOWsp0TStZsRupSi/89XLCr39gUNNpBR96bx7vdp7bGtiLwnNOP9pKfql479kzbuNkKx/LGIae OOE3qtnNlcY8UG8cSpuDCYYWknEs9da+52PCW44EOJaUM4fD409V/0snZePPpCP6AevE=; Original-Received: from ulf.uib.no (smtp.uib.no) [2001:700:200:6::136] by alfons.uib.no with esmtp (Exim 4.92.3) id 1iUoiE-00024s-E1; Wed, 13 Nov 2019 10:13:19 +0100 Original-Received: from zalf.uib.no [129.177.6.94]:43894 by smtp.uib.no with esmtps (Exim 4.92.3) id 1iUoiC-0005N9-Ud; Wed, 13 Nov 2019 10:13:16 +0100 Original-Received: from apache by zalf.uib.no with local (Exim 4.92.3) id 1iUoiC-0004BK-T4; Wed, 13 Nov 2019 10:13:16 +0100 Original-Received: from 114.92-221-204.customer.lyse.net (114.92-221-204.customer.lyse.net [92.221.204.114]) by impmail.uib.no (Horde Framework) with HTTP; Wed, 13 Nov 2019 10:13:16 +0100 Content-Disposition: inline X-checked-clean: by exiscan on alfons.uib.no X-Scanner: 8ce8b252d39948ec6d3c8fb77b174c72 http://tjinfo.uib.no/virus.html X-UiB-SpamFlag: NO UIB: -18.1 hits, 8.0 required X-UiB-SpamReport: spamassassin found; -0.1 uib.no -15 From is listed in 'whitelist_SA' -3.0 Message received from Norway X-Validation-by: yves.bertot@inria.fr X-Loop: coq-club@inria.fr X-Sequence: 18210 Errors-to: coq-club-owner@inria.fr Precedence: list Precedence: bulk Original-Sender: coq-club-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: X-Gmane-Expiry: 2019-11-27 Xref: news.gmane.org gmane.science.mathematics.logic.coq.club:22725 gmane.comp.lang.agda:11356 gmane.science.mathematics.categories:10043 gmane.comp.science.types.announce:8743 Archived-At: After several requests, we extend the deadline to 24 November 2019. Open call for papers Post-proceedings of the 25th International Conference on Types for Proofs and Programs TYPES 2019 TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2019 was held 11-14 June in Oslo, Norway. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings (http://www.dagstuhl.de/en/publications/lipics). Submission to this post-proceedings volume is open to everyone, also to those who did not participate in the conference. We welcome high-quality descriptions of original work, as well as position papers, overview papers, and system descriptions. Submissions should be written in English, not overlapping with published or simultaneously submitted work to a journal or a conference with archival proceedings. The scope of the post-proceedings is the same as the scope of the conference: the theory and practice of type theory. In particular, we welcome submissions on the following topics: * Foundations of type theory and constructive mathematics; * Homotopy type theory and univalent 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; * Formalizing mathematics using type theory. IMPORTANT DATES * Paper and abstract submission: 24 November 2019 * Author notification: 25 March 2020 DETAILS * Papers have to be formatted with LIPIcs style (currently lipics-v2019.cls) and adhere to the style requirements of LIPIcs: http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/ * The upper limit for the length of submissions is 20 pages * Papers have to be submitted in pdf through EasyChair: https://easychair.org/conferences/?conf=types2019postproc * Authors have the option to attach to their submission a zip or tgz file containing code (formalized proofs or programs), but reviewers are not obliged to take the attachments into account and they will not be published. * In case of questions, e.g. on the page limit, contact one of the editors. EDITORS Marc Bezem, Marc.Bezem@uib.no, University of Bergen, Norway Assia Mahboubi, assia.mahboubi@inria.fr, Inria -- Vrije Universiteit Amsterdam