From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10546 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Riccardo Treglia Newsgroups: gmane.comp.science.types.announce,gmane.comp.lang.agda,gmane.science.mathematics.categories,gmane.science.mathematics.prooftheory Subject: ITRS Call for Post-Proceedings Date: Wed, 1 Sep 2021 21:34:35 +0200 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============7024467965414272107==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="37212"; mail-complaints-to="usenet@ciao.gmane.io" To: eutypes-Mttm5w9jbbk@public.gmane.org, agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org, types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org, linear-UfE5FQABeHN2Qaki92YDXw@public.gmane.org, ProofTheory-nJFXYWEDAR8wZN84zEGlPg@public.gmane.org, theory-logic-ETDLCGt7PQU3uPMLIKxrzw@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 Thu Sep 02 22:35:36 2021 Return-path: Envelope-to: gcst-types-announce@m.gmane-mx.org Original-Received: from mx0a-00390e01.pphosted.com ([148.163.133.158]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1mLtQt-0009OG-Ja for gcst-types-announce@m.gmane-mx.org; Thu, 02 Sep 2021 22:35:36 +0200 Original-Received: from pps.filterd (m0172791.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.16.0.43/8.16.0.43) with SMTP id 182KGSi6019841; Thu, 2 Sep 2021 16:34:44 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0a-00390e01.pphosted.com with ESMTP id 3atdxcamrf-1; Thu, 02 Sep 2021 16:34:43 -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 182KYZm9105087; Thu, 2 Sep 2021 16:34:35 -0400 Original-Received: from RHIZOME.SEAS.UPENN.EDU (localhost.upenn.edu [127.0.0.1]) by RHIZOME.seas.upenn.edu (8.16.1/8.15.2) with ESMTP id 182KYZ7R102819; Thu, 2 Sep 2021 16:34:35 -0400 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.16.1/8.15.2) with ESMTP id 181JYtS1093613 for ; Wed, 1 Sep 2021 15:34:56 -0400 Original-Received: from pps.filterd (m0172792.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.16.0.43/8.16.0.43) with SMTP id 181JWlkV010386 for ; Wed, 1 Sep 2021 15:34:55 -0400 Original-Received: from mail-ej1-f46.google.com (mail-ej1-f46.google.com [209.85.218.46]) by mx0a-00390e01.pphosted.com with ESMTP id 3atdxha0mv-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Wed, 01 Sep 2021 15:34:55 -0400 Original-Received: by mail-ej1-f46.google.com with SMTP id a25so1525521ejv.6 for ; Wed, 01 Sep 2021 12:34:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=unito.it; s=google; h=mime-version:from:date:message-id:subject:to; bh=OVzIlyDLdwNmcHkLhk8mjzJpp/Y/SFeqWLQWVO+pUWw=; b=XAEKDrQEqm0Uryen/HnehiNnFzubFS2tvx+qWMjWKQicihi5DTiel2y0KQCfWlJ9w2 2hZ7naxyeIEg5uqk6BI12LOpdsLR6/4bpGFwr/F2nJOuheTosSJ1j2bKP4L0sYZsEv+A WdNBJ8BigmTgneNxlqo3Pu8ZG1lDWs1omtMQU= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=OVzIlyDLdwNmcHkLhk8mjzJpp/Y/SFeqWLQWVO+pUWw=; b=AJUFV+ZusgAoBE4Xe7Avm+CJpmcFq2ehNESj20vKhjFB+QG8DqrCXXNK2OZQ7RbBpP j93bkh8ucymqjjkd9/ZppmVwljFXSaCSGTyFI+4tj2lm7URGwMYelj4K5cHbq0t5Y7hb 34ZBfZ+QNbj8snFsBI9ylLtml627t+0yWsbgsXeMqhsJWmQgG/5Tia5gdRa6LcoMoa8B yaJdvnHt5oWQhAed0y+d+zoEXTYJLPbfGxErTFTaWbVJuUVC+XQYMrbUTMHoXWn4LOPA a9PSXDyAuxr8Y0CRqEDzA8bVMJtyENdGVRC/Rd28ZK6RCi8XnQqbTV9+//EV9S+ZfVbF BzGQ== X-Gm-Message-State: AOAM532F8p7xwwpL3vGBY3gN3V/hlv+ykNXLB8dYBfppaubYY1nCNxbA 0xurwKSjNeRunuKCtseiXihk5uHSe6daf7oydGEhJg== X-Google-Smtp-Source: ABdhPJyF3bup4oWMDrERCZDxAYifFdKWv+TKBz9598vlZ1qjsEYbgpF18QsFJ8Bz/B5x1PrJO6ojjmDPizo0Z2RmTNk= X-Received: by 2002:a17:906:249a:: with SMTP id e26mr1161401ejb.221.1630524893002; Wed, 01 Sep 2021 12:34:53 -0700 (PDT) X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391, 18.0.790 definitions=2021-09-01_05:2021-09-01, 2021-09-01 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 spamscore=0 impostorscore=0 malwarescore=0 phishscore=0 suspectscore=0 clxscore=166 priorityscore=0 bulkscore=0 mlxscore=0 mlxlogscore=836 adultscore=0 lowpriorityscore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2108310000 definitions=main-2109010112 X-Mailman-Approved-At: Thu, 02 Sep 2021 16:34:32 -0400 X-BeenThere: types-announce-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org X-Mailman-Version: 2.1.34 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-ORIG-GUID: 2j2j1125F0qy-CBs68ynA8Um5ZuxF1fC X-Proofpoint-GUID: 2j2j1125F0qy-CBs68ynA8Um5ZuxF1fC X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391,18.0.790 definitions=2021-09-02_04:2021-09-02,2021-09-02 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 mlxlogscore=999 priorityscore=1501 mlxscore=0 lowpriorityscore=0 clxscore=1011 suspectscore=0 malwarescore=0 spamscore=0 phishscore=0 bulkscore=0 impostorscore=0 adultscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2108310000 definitions=main-2109020116 Xref: news.gmane.io gmane.comp.science.types.announce:9821 gmane.comp.lang.agda:12730 gmane.science.mathematics.categories:10546 gmane.science.mathematics.prooftheory:1667 Archived-At: --===============7024467965414272107== 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 ] --===============7024467965414272107== Content-Type: multipart/alternative; boundary="0000000000000b9d8f05caf429ce" --0000000000000b9d8f05caf429ce Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable ITRS 2021 Call for Post-ProceedingsTenth Workshop on Intersection Types and Related Systems - ITRS 2021 17 July 2021, Online Affiliated with FSCD , 17-24 July 2021, Buenos Aires Web page: https://urldefense.com/v3/__http://www.di.unito.it/*deligu/ITRS20= 21/__;fg!!IBzWLUs!AR_MVm7M1emYukg5-ncWfFC6B2TnQeW6IDRSf1zYYJEA4kOsvG_PBUUyI= THn2U2YUo-7l8D8xCybkw$=20 Aims and Scope Intersection types were introduced near the end of the 1970s to overcome the limitations of Curry's type assignment system and to provide a characterization of the strongly normalizing terms of the Lambda Calculus. The key idea is to introduce an intersection type constructor =E2=88=A7 suc= h that a term of type t =E2=88=A7 s can be used at both type t and s within the same context. This provides a finite polymorphism where various, even unrelated, types of the term are listed explicitly, differently from the more widely used universally quantified types where the polymorphic type is the common schema that stands for its various type instances. As a consequence, more terms (all and only the normalizing terms) can be typed than with universal polymorphism. Although intersection types were initially intended for use in analyzing and/or synthesizing lambda models as well as in analyzing normalization properties, over the last twenty years the scope of the research on intersection types and related systems has broadened in many directions. Restricted (and more manageable) forms have been investigated, such as refinement types. Type systems based on intersection type theory have been extensively studied for practical purposes, such as program analysis and higher-order model checking. The dual notion of union types turned out to be quite useful for programming languages. Finally, the behavioral approach to types, which can give a static specification of computational properties, has become central in the most recent research on type theory. The ITRS 2021 workshop aims to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches. Possible topics for submitted papers include, but are not limited to: - Formal properties of systems with intersection types. - Results for related systems, such as union types, refinement types, or singleton types. - Applications to lambda calculus, pi-calculus and similar systems. - Applications for programming languages, program analysis, and program verification. - Applications for other areas, such as database query languages and program extraction from proofs. - Related approaches using behavioral/intensional types and/or denotational semantics to characterize computational properties. - Quantitative refinements of intersection types. ITRS workshops have been held every two years (with the exception of 2020, because of COVID-19 outbreak). Information about the previous events is available on the ITRS home page . Post-Proceedings We are planning post-proceedings, including presentations to the workshop and submissions accepted via an open call with *dates*: - submission deadline: *1 October* - acceptance communication: *5 November* - camera-ready version: *19 November* Papers should not be published elsewhere, with original results or surveying ongoing research. They should be written in English using LaTex and will appear on EPTCS: see Information for Authors . Sub= missions should be 20 pages long, excluding bibliography and avoiding technical appendices. Submissions are expected via EasyChair . Program Committee - Antonio Bucciarelli, Universit=C3=A9 de Paris, France - Daniel de Carvalho, Universit=C3=A9 Grenoble Alpes, France - Andrej Dudenhefner, Saarland University, Germany - Silvia Ghilezan, University of Novi Sad, Serbia - Giulio Guerrieri, University of Bath, UK - Ugo de' Liguoro, Universit=C3=A0 di Torino, Italy (chair) - Jeremy Siek, Indiana University Bloomington, USA (co-chair) ------------------------------ Steering Committee - Mariangiola Dezani-Ciancaglini, Universit=C3=A0 di Torino, Italy - Jakob Rehof, TU University of Dortmund, Germany - Joe Wells, Heriot-Watt University, Scotland Organizers: - Ugo de' Liguoro, Universit=C3=A0 di Torino, Italy - Riccardo Treglia, Universit=C3=A0 di Torino, Italy ( riccardo.treglia-Ob+gDNbliO0@public.gmane.org) --0000000000000b9d8f05caf429ce Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable

ITRS 2021 Call for Post-Proceedings

Tent= h Workshop on Intersection Types and Related Systems - ITRS 2021

17 July 2021, Online

Affilia= ted with=C2=A0FSCD, 17-24 Jul= y 2021, Buenos Aires

Web page:=C2=A0http://www.di.unito.it/~delig= u/ITRS2021/

Aims and Scope

Intersection types were i= ntroduced near the end of the 1970s to overcome the limitations of Curry= 9;s type assignment system and to provide a characterization of the strongl= y normalizing terms of the Lambda Calculus. The key idea is to introduce an= intersection type constructor =E2=88=A7 such that a term of type t =E2=88= =A7 s can be used at both type t and s within the same context. This provid= es a finite polymorphism where various, even unrelated, types of the term a= re listed explicitly, differently from the more widely used universally qua= ntified types where the polymorphic type is the common schema that stands f= or its various type instances. As a consequence, more terms (all and only t= he normalizing terms) can be typed than with universal polymorphism.

Although intersection types were initially intended f= or use in analyzing and/or synthesizing lambda models as well as in analyzi= ng normalization properties, over the last twenty years the scope of the re= search on intersection types and related systems has broadened in many dire= ctions. Restricted (and more manageable) forms have been investigated, such= as refinement types. Type systems based on intersection type theory have b= een extensively studied for practical purposes, such as program analysis an= d higher-order model checking. The dual notion of union types turned out to= be quite useful for programming languages. Finally, the behavioral approac= h to types, which can give a static specification of computational properti= es, has become central in the most recent research on type theory.

The ITRS 2021 workshop aims to bring together researche= rs working on both the theory and practical applications of systems based o= n intersection types and related approaches. Possible topics for submitted = papers include, but are not limited to:

  • Formal properties of systems with inte= rsection types.
  • Results for related systems, s= uch as union types, refinement types, or singleton types.
  • Applications to lambda calculus, pi-calculus and similar system= s.
  • Applications for programming languages, pro= gram analysis, and program verification.
  • Appli= cations for other areas, such as database query languages and program extra= ction from proofs.
  • Related approaches using be= havioral/intensional types and/or denotational semantics to characterize co= mputational properties.
  • Quantitative refinemen= ts of intersection types.

ITRS workshops = have been held every two years (with the exception of 2020, because of COVI= D-19 outbreak). Information about the previous events is available on the= =C2=A0ITRS home page.

Post-Proceedings

We are planning post-proceedings, including pres= entations to the workshop and submissions accepted via an open call with=C2= =A0dates:

    <= li style=3D"margin:0px">submission deadline:=C2=A01 October
  • acceptance communic= ation:=C2=A05 November
  • camera-ready version:=C2=A019 November

Papers should no= t be published elsewhere, with original results or surveying ongoing resear= ch. They should be written in English using LaTex and will appear on EPTCS:= see=C2=A0Information for Authors.= Submissions should be 20 pages long, excluding bibliography and avoiding t= echnical appendices. Submissions are expected via=C2=A0EasyChair.

Program Committee

  • Antonio B= ucciarelli, Universit=C3=A9 de Paris, France
  • D= aniel de Carvalho, Universit=C3=A9 Grenoble Alpes, France
  • Andrej Dudenhefner, Saarland University, Germany
  • Silvia Ghilezan, University of Novi Sad, Serbia
  • Giulio Guerrieri, University of Bath, UK
  • Ugo de' Liguoro, Universit=C3=A0 di Torino, Italy (chair)<= /li>
  • Jeremy Siek, Indiana University Bloomington, U= SA (co-chair)

    • Steering Committee

    • Mariangiola De= zani-Ciancaglini, Universit=C3=A0 di Torino, Italy
    • Jakob Rehof, TU University of Dortmund, Germany
    • Joe Wells, Heriot-Watt University, Scotland

    =

    Organizers:

    --0000000000000b9d8f05caf429ce-- --===============7024467965414272107==--