From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10464 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 21 - Final CfP Date: Tue, 20 Apr 2021 10:00:31 +0200 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============6436262092904908829==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="28852"; 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 Apr 22 19:03:10 2021 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 1lZcjN-0007Bf-Sb for gcst-types-announce@m.gmane-mx.org; Thu, 22 Apr 2021 19:03:10 +0200 Original-Received: from pps.filterd (m0128480.ppops.net [127.0.0.1]) by mx0b-000c2a01.pphosted.com (8.16.1.2/8.16.1.2) with SMTP id 13MGp2eu015728; Thu, 22 Apr 2021 13:01:56 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0b-000c2a01.pphosted.com with ESMTP id 382xv9r6vj-1; Thu, 22 Apr 2021 13:01:53 -0400 Original-Received: from RHIZOME.seas.upenn.edu (RHIZOME.SEAS.UPENN.EDU [158.130.69.24]) by leopard.seas.upenn.edu (8.16.1/8.15.2) with ESMTP id 13MH1f2L022916; Thu, 22 Apr 2021 13:01:41 -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 13MH1fAk026861; Thu, 22 Apr 2021 13:01:41 -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.16.1/8.15.2) with ESMTP id 13K81GJI044726 for ; Tue, 20 Apr 2021 04:01:16 -0400 Original-Received: from pps.filterd (m0172794.ppops.net [127.0.0.1]) by mx0b-00390e01.pphosted.com (8.16.0.43/8.16.0.43) with SMTP id 13K7utR0032061 for ; Tue, 20 Apr 2021 04:01:16 -0400 Original-Received: from mail-ed1-f41.google.com (mail-ed1-f41.google.com [209.85.208.41]) by mx0b-00390e01.pphosted.com with ESMTP id 380cp1a23r-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Tue, 20 Apr 2021 04:01:16 -0400 Original-Received: by mail-ed1-f41.google.com with SMTP id g17so43201978edm.6 for ; Tue, 20 Apr 2021 01:01:15 -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=znW9Pa2QxA7gYJKs+x11ksJxcb1TKDamPEfU5FfoILQ=; b=jQBBQHaHvcLq/1dLRc+zL9bhSXHVZfzDE6d6sqSIoZhAnpb1qOkerwOaFBZqvq/Ptm KZyK2HpfnmAarL7iNu0xzIxBMyrF5XoNOG7e0hiZedizm+okoiqCJBXYAYQJjSqu8Rpj RjoZPDCdcivXtvzC55s11OLBnb7dGy3w9d4YU= 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=znW9Pa2QxA7gYJKs+x11ksJxcb1TKDamPEfU5FfoILQ=; b=hNJ7t4OaP+KAW3YRfBicQHiMAb4QoiD3aGfxwaD1dBqCsCAOvWzAKOl7SnidOuzkB2 mPT4SlsNkbAQSExq9UxUqXqIb07mdF5yGrBQgOiV+A0bXeJ2Q/trkwn0FlUvDiB7Qpgw 1KCQNbjOiLELN16jBA2AbjNHYt1YdkARjiuFGc3gCOFD9xiGdoovYMb3rgsIgvdIopos uvyykMuvTKwL/vb7xhHhzYFAeO20/wK1YsviEQ8+3i1XUnyX6K1rmo7zyF1aHOGsvXVX JtIMd+sy/5Z0mT+eFo+2KrcHWbRVC2mGN5oJBWo7Ht78fef2N9OoPR2W7G3tFaPHw8Vp O6bg== X-Gm-Message-State: AOAM531qZKlxQCg2oITDnz+NM00YxwYMGdqvxR75pWMKi/VruE/eLEIU 87FNWqo7FQ3C2w/Ai20wlrXaaiaBC4uAK9d1zZh1Cg== X-Google-Smtp-Source: ABdhPJxb3pFID/fvbZfA8XkQ/ccnLWY196F9AH/b3fAGg330CN+c455e3HdQuwBgd/6xt3ONjzqfFMaKGUjLQrk14yU= X-Received: by 2002:aa7:d046:: with SMTP id n6mr30136009edo.357.1618905674243; Tue, 20 Apr 2021 01:01:14 -0700 (PDT) X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391, 18.0.761 definitions=2021-04-20_02:2021-04-19, 2021-04-20 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 mlxscore=0 priorityscore=0 bulkscore=0 adultscore=0 lowpriorityscore=0 suspectscore=0 spamscore=0 clxscore=330 malwarescore=0 mlxlogscore=999 impostorscore=0 phishscore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2104060000 definitions=main-2104200061 X-Mailman-Approved-At: Thu, 22 Apr 2021 13:01:39 -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-GUID: WutfO54On43FVpcsn5-ti0N3UWrmKwZF X-Proofpoint-ORIG-GUID: WutfO54On43FVpcsn5-ti0N3UWrmKwZF X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.136,Aquarius:18.0.761,Hydra:6.0.391,FMLib:17.0.607.475 definitions=2021-04-22_11,2021-04-22_01,2020-04-07_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 bulkscore=0 mlxscore=0 phishscore=0 lowpriorityscore=0 suspectscore=0 adultscore=0 clxscore=1011 impostorscore=0 spamscore=0 priorityscore=1501 mlxlogscore=999 malwarescore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2104060000 definitions=main-2104220128 Xref: news.gmane.io gmane.comp.science.types.announce:9589 gmane.comp.lang.agda:12572 gmane.science.mathematics.categories:10464 gmane.science.mathematics.prooftheory:1655 Archived-At: --===============6436262092904908829== 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 ] --===============6436262092904908829== Content-Type: multipart/alternative; boundary="000000000000a3759a05c062d979" --000000000000a3759a05c062d979 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable ITRS 2021 Call for papersTenth Workshop on Intersection Types and Related Systems - ITRS 2021 17 July 2021, Online Affiliated with FSCD , 17-24 July 2021, Buenos Aires Web page: http://www.di.unito.it/~deligu/ITRS2021/ 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 behavioural 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 behavioural/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 . Invited Speaker - Jeremy Siek (Indiana University Bloomington) Paper Submissions Papers must be original and not previously published, nor submitted elsewhere. Papers should be prepared in LaTeX using the EPTCS macro package and should be in the range of 3-16 pages, plus at most 2 pages of references. Submissions will be collected via EasyChair and reviewed by anonymous referees. Important Dates - Paper submission: 12 April *26 April 2021 (extended)* - Author notification: 24 May 2021 - Final version: 18 June 2021 - Workshop: 17 July 2021 Program Committee - Antonio Bucciarelli, Universit=C3=A9 de Paris, France - Daniel De Carvalho, Innopolis University, Russia - 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) Organizers: Ugo de' Liguoro, Universit=C3=A0 di Torino, Italy Riccardo Treglia, Universit=C3=A0 di Torino, Italy (riccardo.treglia@unito.= it) Steering Committee - Mariangiola Dezani-Ciancaglini, Universit=C3=A0 di Torino, Italy - Jakob Rehof, TU University of Dortmund, Germany - Joe Wells, Heriot-Watt University, Scotland --000000000000a3759a05c062d979 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

ITRS 2021 Call for papers

Tenth Workshop= on Intersection Types and Related Systems - ITRS 2021

17 July 2021, Online

Affiliated with= =C2=A0FSCD, 17-24 July 2021, Buenos Aires

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

Aims and Scope

=

Intersection types were introduced near the end of= the 1970s to overcome the limitations of Curry's type assignment syste= m and to provide a characterization of the strongly normalizing terms of th= e Lambda Calculus. The key idea is to introduce an intersection type constr= uctor =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 provides a finite polymorphism w= here various, even unrelated, types of the term are listed explicitly, diff= erently from the more widely used universally quantified types where the po= lymorphic type is the common schema that stands for its various type instan= ces. As a consequence, more terms (all and only the normalizing terms) can = be typed than with universal polymorphism.

Alth= ough intersection types were initially intended for use in analyzing and/or= synthesizing lambda models as well as in analyzing normalization propertie= s, over the last twenty years the scope of the research on intersection typ= es and related systems has broadened in many directions. Restricted (and mo= re manageable) forms have been investigated, such as refinement types. Type= systems based on intersection type theory have been extensively studied fo= r practical purposes, such as program analysis and higher-order model check= ing. The dual notion of union types turned out to be quite useful for progr= amming languages. Finally, the behavioural approach to types, which can giv= e a static specification of computational properties, has become central in= the most recent research on type theory.

The I= TRS 2021 workshop aims to bring together researchers working on both the th= eory and practical applications of systems based on intersection types and = related approaches. Possible topics for submitted papers include, but are n= ot limited to:

  • Formal properties of systems with intersection types.
  • Results for related systems, such as union types, refin= ement types, or singleton types.
  • Applications = to lambda calculus, pi-calculus and similar systems.
  • Applications for programming languages, program analysis, and progra= m verification.
  • Applications for other areas, = such as database query languages and program extraction from proofs.
    • Related approaches using behavioural/intensional typ= es and/or denotational semantics to characterize computational properties.<= /li>
  • Quantitative refinements of intersection types= .

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

Invited Speaker<= /h3>
  • Je= remy Siek (Indiana University Bloomington)

Paper Submissions

Papers must be original and not previously published, nor submit= ted elsewhere. Papers should be prepared in LaTeX using the=C2=A0EPTCS macro= =C2=A0package and should be in the range of 3-16 pages, plus at most 2 page= s of references. Submissions will be collected via=C2=A0EasyChair=C2=A0and reviewed by anonymous referees.

Important Dates

  • Paper submissio= n:=C2=A012 April=C2=A026 April 2021 (ext= ended)
  • Author notification: 24 May 2021
  • Final version: 18 June 2021
  • Workshop: 17 July 2021

Program Committee

  • Antonio Bucciarelli, Universit= =C3=A9 de Paris, France
  • Daniel De Carvalho, In= nopolis University, Russia
  • Andrej Dudenhefner,= Saarland University, Germany
  • Silvia Ghilezan,= University of Novi Sad, Serbia
  • Giulio Guerrie= ri, University of Bath, UK
  • Ugo de' Liguoro= , Universit=C3=A0 di Torino, Italy (chair)
  • Jer= emy Siek, Indiana University Bloomington, USA (co-chair)

Organizers:

Ugo de' Liguoro, Universit=C3=A0 di Torino, Italy

Riccardo Treglia, Universit=C3=A0 di Torino, Ital= y (riccardo.treglia-Ob+gDNbliO0@public.gmane.org)

Steeri= ng Committee

--000000000000a3759a05c062d979-- --===============6436262092904908829==--