From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10119 Path: news.gmane.io!.POSTED.ciao.gmane.io!not-for-mail From: Ugo de Liguoro Newsgroups: gmane.comp.science.types.announce,gmane.comp.lang.agda,gmane.science.mathematics.categories,gmane.science.mathematics.logic.isabelle.user,gmane.science.mathematics.prooftheory,gmane.science.mathematics.logic.coq.club Subject: TYPES and ITRS - Call for participation Date: Tue, 28 Jan 2020 10:07:39 +0100 Message-ID: <96f6c7d0-e486-2db4-a62c-4859e1983b9e@di.unito.it> Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-15"; Format="flowed" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="ciao.gmane.io:159.69.161.202"; logging-data="74488"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:68.0) Gecko/20100101 Thunderbird/68.4.1 To: eutypes-Mttm5w9jbbk@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, coq-club-MZpvjPyXg2s@public.gmane.org Original-X-From: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Tue Jan 28 11:19:20 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 1iwNxn-000JJK-FO for gcst-types-announce@m.gmane-mx.org; Tue, 28 Jan 2020 11:19:19 +0100 Original-Received: from pps.filterd (m0128480.ppops.net [127.0.0.1]) by mx0b-000c2a01.pphosted.com (8.16.0.42/8.16.0.42) with SMTP id 00SAHqrt001387; Tue, 28 Jan 2020 05:18:34 -0500 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0b-000c2a01.pphosted.com with ESMTP id 2xrgsys98p-1; Tue, 28 Jan 2020 05:18:34 -0500 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 00SAIUld001479; Tue, 28 Jan 2020 05:18:32 -0500 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 00SAIPAn031856; Tue, 28 Jan 2020 05:18:28 -0500 X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $ Original-Received: from mx0a-00390e01.pphosted.com (mx0a-00390e01.pphosted.com [148.163.133.158]) by RHIZOME.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 00S99Enf023131 for ; Tue, 28 Jan 2020 04:09:14 -0500 Original-Received: from pps.filterd (m0172792.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.16.0.42/8.16.0.42) with SMTP id 00S99D51031738 for ; Tue, 28 Jan 2020 04:09:13 -0500 Original-Received: from mail.di.unito.it (pianeta.di.unito.it [130.192.156.1]) by mx0a-00390e01.pphosted.com with ESMTP id 2xrg619wh2-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Tue, 28 Jan 2020 04:09:13 -0500 X-MailScanner-From: deligu-2eFfYwgyqgY1GQ1Ptb7lUw@public.gmane.org X-SpamCheck: not spam, SpamAssassin (not cached, score=-102.095, required 3, autolearn=not spam, ALL_TRUSTED -1.00, AUTHENTICATEDUSER -100.00, AWL 0.80, BAYES_00 -1.90, URIBL_BLOCKED 0.00) X-AntiVirus: Email Clean X-dipinfo-MailScanner-ID: 00S97dn4018166 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 00S97dn4018166 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO AuthenticatedUser=deligu ); Tue, 28 Jan 2020 10:07:39 +0100 (CET) DKIM-Filter: OpenDKIM Filter v2.11.0 mail.di.unito.it 00S97dn4018166 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=di.unito.it; s=dipinfo2011; t=1580202463; bh=3T4s+qhZRzshfb/9+4W44X23xkEmPT+6anaWKCyqDFs=; h=From:Subject:To:Date; b=EfDAMFmMx40Vu7gV23UReGsNYpZ617PXdQC03kW7TpwlkwLJJvruCvX4lNXBFKQDe LrxBvhfs02e1Uu2TLxuiaCdNLEd/0CHAprZs78NYMbsczJQDhvcuvWTsaaJlkbsOAN nXYe91n29AV0iAVerdCVWFUsnkljAUoAd4AFAca8= Content-Language: it X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.138, 18.0.572 definitions=2020-01-28_02:2020-01-24, 2020-01-28 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 phishscore=0 clxscore=185 adultscore=0 impostorscore=0 priorityscore=0 spamscore=0 lowpriorityscore=98 mlxscore=0 mlxlogscore=884 suspectscore=0 bulkscore=98 malwarescore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-1911200001 definitions=main-2001280076 X-Mailman-Approved-At: Tue, 28 Jan 2020 05:18:24 -0500 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.138,18.0.572 definitions=2020-01-28_02:2020-01-24,2020-01-28 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 malwarescore=0 adultscore=0 lowpriorityscore=1 mlxscore=0 suspectscore=0 priorityscore=1501 mlxlogscore=999 phishscore=0 clxscore=1011 spamscore=0 impostorscore=0 bulkscore=1 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-1911200001 definitions=main-2001280083 Xref: news.gmane.io gmane.comp.science.types.announce:8886 gmane.comp.lang.agda:11491 gmane.science.mathematics.categories:10119 gmane.science.mathematics.logic.isabelle.user:17906 gmane.science.mathematics.prooftheory:1635 gmane.science.mathematics.logic.coq.club:22915 Archived-At: [ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Apologies for multiple recipiens =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D --------------------------------------------------------------------- Call For Participation to TYPES 2020 --------------------------------------------------------------------- =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D 26th INTERNATIONAL CONFERENCE ON TYPES FOR PROOFS AND PROGRAMS 2020 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D https://types2020.di.unito.it Turin, Italy, TYPES 2-5 March and ITRS 6 March 2020 The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The TYPES areas of interest include, but are not limited to: * 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; * formalizing mathematics using type theory. We host talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress. The EUTypes Cost Action CA15123 (eutypes.cs.ru.nl) focuses on the same research topics as TYPES and partially sponsors the TYPES Conference: Part of the program is organised under the auspices of EUTypes. INVITED SPEAKERS * Ulrik Buchholtz * Pierre Marie-P=E9drot * Leonardo de Moura * Sara Negri The ITRS 2020 workshop aims to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches. Topics include, but are not limited to: =A0=A0=A0 Formal properties of systems with intersection types. =A0=A0=A0 Results for related systems, such as union types, refinement typ= es, = or singleton types. =A0=A0=A0 Applications to lambda calculus, pi-calculus and similar systems. =A0=A0=A0 Applications for programming languages, program analysis, and = program verification. =A0=A0=A0 Applications for other areas, such as database query languages a= nd = program extraction from proofs. =A0=A0=A0 Related approaches using behavioural/intensional types and/or = denotational semantics to characterize =A0=A0=A0 computational properties. =A0=A0=A0 Quantitative refinements of intersection types. Invited Speaker - Jeremy Siek (Indiana University Bloomington) Registration form: https://types2020.di.unito.it/registration.html Early registration: 12th February CONTACT Ugo de'Liguoro Email: ugo.deliguoro-Ob+gDNbliO0@public.gmane.org -- = Ugo de'Liguoro Associate Professor of Computer Science Dipartimento di Informatica Universit=E0 di Torino Corso Svizzera 185, 10149, Torino, Italy