From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10299 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: "Ugo de'Liguoro" Newsgroups: gmane.comp.science.types.announce,gmane.science.mathematics.logic.coq.club,gmane.comp.lang.agda,gmane.science.mathematics.categories,gmane.science.mathematics.logic.isabelle.user,gmane.science.mathematics.prooftheory Subject: CfP for TYPES 2020 postproceedings: Date: Fri, 9 Oct 2020 23:15:22 +0200 Message-ID: <5d06ca73-9c8d-8deb-9a15-f6a007488b56@di.unito.it> Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============1981757061897569376==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="31189"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:68.0) Gecko/20100101 Thunderbird/68.12.1 To: eutypes-Mttm5w9jbbk@public.gmane.org, coq-club-MZpvjPyXg2s@public.gmane.org, agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org, types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org, moca-announce-HnE2qM1WCGmhtn/xwUALyw@public.gmane.org, linear-UfE5FQABeHN2Qaki92YDXw@public.gmane.org, cl-isabelle-users-33AaDErTWvBK/gkPnarB6Q@public.gmane.org, ProofTheory-0VDFhBbLC1Y8tAQEoGlWAQ@public.gmane.org, theory-logic-ddtmkgJwdYjltQq4i4S/Dg@public.gmane.org, logic-o02PS0xoJP/q4qjOmvqfQQ@public.gmane.org, theorem-provers-iSp611qFfoI3uPMLIKxrzw@public.gmane.org Original-X-From: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Sat Oct 10 06:52:58 2020 Return-path: Envelope-to: gcst-types-announce@m.gmane-mx.org Original-Received: from mx0b-000c2a01.pphosted.com ([148.163.155.36]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1kR6sM-0007x8-Fx for gcst-types-announce@m.gmane-mx.org; Sat, 10 Oct 2020 06:52:58 +0200 Original-Received: from pps.filterd (m0128480.ppops.net [127.0.0.1]) by mx0b-000c2a01.pphosted.com (8.16.0.43/8.16.0.43) with SMTP id 09A4l3qQ009225; Sat, 10 Oct 2020 00:52:01 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0b-000c2a01.pphosted.com with ESMTP id 3429herejv-1; Sat, 10 Oct 2020 00:52:01 -0400 Original-Received: from RHIZOME.seas.upenn.edu (RHIZOME.SEAS.UPENN.EDU [158.130.69.24]) by leopard.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 09A4pmpo106125; Sat, 10 Oct 2020 00:51:48 -0400 Original-Received: from RHIZOME.SEAS.UPENN.EDU (localhost.upenn.edu [127.0.0.1]) by RHIZOME.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 09A4pmKf058918; Sat, 10 Oct 2020 00:51:48 -0400 X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $ Original-Received: from mx0b-00390e01.pphosted.com (mx0b-00390e01.pphosted.com [148.163.137.158]) by RHIZOME.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 099LG5Kr123675 for ; Fri, 9 Oct 2020 17:16:05 -0400 Original-Received: from pps.filterd (m0172794.ppops.net [127.0.0.1]) by mx0b-00390e01.pphosted.com (8.16.0.42/8.16.0.42) with SMTP id 099LFvhb025897 for ; Fri, 9 Oct 2020 17:16:05 -0400 Original-Received: from mail.di.unito.it (pianeta.di.unito.it [130.192.156.1]) by mx0b-00390e01.pphosted.com with ESMTP id 3429jv5t39-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Fri, 09 Oct 2020 17:16:05 -0400 X-MailScanner-From: deligu-2eFfYwgyqgY1GQ1Ptb7lUw@public.gmane.org X-SpamCheck: not spam, SpamAssassin (not cached, score=-102.128, required 3, autolearn=not spam, ALL_TRUSTED -1.00, AUTHENTICATEDUSER -100.00, AWL 0.77, BAYES_00 -1.90, HTML_MESSAGE 0.00) X-AntiVirus: Email Clean X-dipinfo-MailScanner-ID: 099LFMQx018938 X-dipinfo-MailScanner-Information: Please contact Department of Computer Science technical staff for more information Original-Received: from mail.di.unito.it ([130.192.156.1]) by mail.di.unito.it (INFO-DIP) with ESMTPSA id 099LFMQx018938 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO AuthenticatedUser=deligu ); Fri, 9 Oct 2020 23:15:23 +0200 (CEST) DKIM-Filter: OpenDKIM Filter v2.11.0 mail.di.unito.it 099LFMQx018938 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=di.unito.it; s=dipinfo2011; t=1602278127; bh=p5TyhgSxFiP25ttfzYu3721oRNbVIPggqmYRIfVtIro=; h=From:To:Subject:Date; b=KpMAjd2Y41PN84x73R8NVTB2LDcbxZP/AxP3G7DpvS2bhAsrzeJQ4cb2i725duX6O CrGmXSAvKdYrNvQ7+lBr0p+8NNB3CRMziOPeB8K97iBJqP3LT5DW66G0emIS3fPsk2 zKqfIsq3m6SgjbMVmRbRky7UAcV3xOHJDez7kDXA= Content-Language: it X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.235, 18.0.687 definitions=2020-10-09_13:2020-10-09, 2020-10-09 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 phishscore=0 mlxscore=0 adultscore=0 lowpriorityscore=0 clxscore=228 spamscore=0 mlxlogscore=999 priorityscore=0 malwarescore=0 bulkscore=0 suspectscore=0 impostorscore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2009150000 definitions=main-2010090155 X-Mailman-Approved-At: Sat, 10 Oct 2020 00:51:46 -0400 X-BeenThere: types-announce-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Announcements of interest to the TYPES community List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Original-Sender: "Types-announce" X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.235,18.0.687 definitions=2020-10-10_01:2020-10-09,2020-10-10 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 bulkscore=0 priorityscore=1501 malwarescore=0 suspectscore=0 clxscore=1011 adultscore=0 impostorscore=0 mlxscore=0 lowpriorityscore=0 phishscore=0 mlxlogscore=999 spamscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2009150000 definitions=main-2010100044 Xref: news.gmane.io gmane.comp.science.types.announce:9240 gmane.science.mathematics.logic.coq.club:23011 gmane.comp.lang.agda:12294 gmane.science.mathematics.categories:10299 gmane.science.mathematics.logic.isabelle.user:17931 gmane.science.mathematics.prooftheory:1640 Archived-At: This is a multi-part message in MIME format. --===============1981757061897569376== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline [ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] --===============1981757061897569376== Content-Type: multipart/alternative; boundary="------------16BECB9F44996276BDE85D99" Content-Language: it This is a multi-part message in MIME format. --------------16BECB9F44996276BDE85D99 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Post-proceedings of the TYPES 2020      26th International Conference on Types for Proofs and Programs                           Open call for papers TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2020 wasn’t held in Turin as planned because of the COVID-19 outbreak. Nonetheless the significant number of submissions and registrations testified the interest for TYPES in our community, motivating us to plan publishing post-proceedings. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics , an open-access series of conference proceedings. Submission to this post-proceedings volume is open to everyone, also to those who did not submit a contribution to 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. We would like to invite all researchers that study and apply type systems to share their results. In particular, we welcome submissions on the following topics: * 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; * Type theory in linguistics. Important dates: * Paper submission: 19 October 31 October 2020 * Author notification: 18 January 2021 * Final version:  15 February 2021 * Publication (presumably): end of March 2021 Details: * Papers have to be written in LaTex and adhere to the style requirements of LIPIcs . * The recommended length of a paper is 12-15 pages, excluding front-page(s) (authors, affiliation, keywords, abstract, ...), bibliography and an appendix of max 5 pages. If you need more pages, please ask the editors. * Papers have to be submitted in pdf through EasyChair: https://easychair.org/conferences/?conf=types2020postproceed * Accepted papers will be charged of 60:00€, according to LIPIcs policy for publication costs (https://www.dagstuhl.de/en/publications/lipics/processing-charge/) * In case of questions, please contact one of the editors. Editors: * Ugo de’Liguoro (Università di Torino) * Stefano Berardi (Università di Torino) * Thorsten Altenkirch (University of Nottingham) -- Ugo de'Liguoro Associate Professor of Computer Science Dipartimento di Informatica Università di Torino Corso Svizzera 185, 10149, Torino, Italy phone +39 011 6706766 - fax: +39 011 751603 --------------16BECB9F44996276BDE85D99 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: 8bit

                          Post-proceedings of the TYPES 2020
     26th International Conference on Types for Proofs and Programs

                          Open call for papers
                         
TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2020 wasn’t held in Turin as planned because of the COVID-19 outbreak. Nonetheless the significant number of submissions and registrations testified the interest for TYPES in our community, motivating us to plan publishing post-proceedings. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings.
Submission to this post-proceedings volume is open to everyone, also to those who did not submit a contribution to 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.
We would like to invite all researchers that study and apply type systems to share their results. In particular, we welcome submissions on the following topics:
  • 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;
  • Type theory in linguistics.
Important dates:
  • Paper submission: 19 October 31 October 2020
  • Author notification: 18 January 2021
  • Final version:  15 February 2021
  • Publication (presumably): end of March 2021
Details:
Editors:
  • Ugo de’Liguoro (Università di Torino)
  • Stefano Berardi (Università di Torino)
  • Thorsten Altenkirch (University of Nottingham) 
-- 
Ugo de'Liguoro
Associate Professor of Computer Science
Dipartimento di Informatica
Università di Torino
Corso Svizzera 185, 10149, Torino, Italy
phone +39 011 6706766 - fax: +39 011 751603
--------------16BECB9F44996276BDE85D99-- --===============1981757061897569376==--