From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10429 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 CfP Date: Thu, 25 Mar 2021 10:15:47 +0100 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============5531847131521640766==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="22687"; 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 Mar 25 13:29:31 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 1lPP7C-0005hs-OT for gcst-types-announce@m.gmane-mx.org; Thu, 25 Mar 2021 13:29:30 +0100 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 12PCM957031235; Thu, 25 Mar 2021 08:28: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 37db9r1v02-1; Thu, 25 Mar 2021 08:28:55 -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 12PCSkX4087750; Thu, 25 Mar 2021 08:28:46 -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 12PCSkjF100832; Thu, 25 Mar 2021 08:28:46 -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 12P9GMI6070153 for ; Thu, 25 Mar 2021 05:16:23 -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 12P9Cvr4028341 for ; Thu, 25 Mar 2021 05:16:22 -0400 Original-Received: from mail-ed1-f43.google.com (mail-ed1-f43.google.com [209.85.208.43]) by mx0a-00390e01.pphosted.com with ESMTP id 37dx5uv06f-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Thu, 25 Mar 2021 05:16:21 -0400 Original-Received: by mail-ed1-f43.google.com with SMTP id o19so1596166edc.3 for ; Thu, 25 Mar 2021 02:16:21 -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=4QpjnJxcOinozsEFMpyDfPMuZ4sPPpdffDReh6/Rh2A=; b=AEi2amo2OHDYPVvKXLfpCnX+xhJG7PF6gnL+OlKl7uiDC//OuRTS/7qt2aSiefkSJA O/yOQEjlPUXOswdqpDVURYD9UZdGGnmQkc8oGe/JEkDwGwNKZ7BCUGmLEanxwk/RpV2V Epq3NJzbigFF4CESSLpLwHkRFWg6iKx44p8n4= 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=4QpjnJxcOinozsEFMpyDfPMuZ4sPPpdffDReh6/Rh2A=; b=Ta9wJNYGSzu4zIekQQwaK/B3zN2yAFennl/HpzOjnCCqPC0EVqRLehF0+O8diLM1h2 A4jP5XUGaG8/ZD5FHDYTSKVTdsbyzgZ03U6luX7ER1LP58qcCgnZyzQRyRjrG/2SyQk+ Y75Xkz5pplPddlBlHUr5fwyaM6tSXSDa8MfdfpoALUeiU0u8SPpFZPIUDEFwSTK2yAAK fvV2Suo0h5FyH1O5UP6C1Sele4zcfAu6HtPCANL4FXL+kymFdFynISRuqifEnPozGhiX l7d04oApaa7RkjDs3JczdCDxjiayGQnpXXNZNBNmJ+yYNhRVI44GEVIfhQCiW3aYsuTl 7sWA== X-Gm-Message-State: AOAM533M8N1jWqNmUVWYwq8KjAdOUttThy1KiHEG5gigyA4/aoOUUYxE k8seASS5B+pbU8jgFsLkIvXUlgXG2bVvhABDE75tgA== X-Google-Smtp-Source: ABdhPJy2iXtclPRYaUuHvmH7lGS8H0q9Bzuj9q1m15uZ2eF4D1RIvLFUOXH6sN/rHJDKkSb15LLttMVfWMr8FpHWY4I= X-Received: by 2002:aa7:c3c1:: with SMTP id l1mr8158691edr.208.1616663779569; Thu, 25 Mar 2021 02:16:19 -0700 (PDT) X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.369, 18.0.761 definitions=2021-03-25_02:2021-03-24, 2021-03-25 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 lowpriorityscore=0 mlxscore=0 priorityscore=0 adultscore=0 clxscore=165 suspectscore=0 impostorscore=0 bulkscore=0 malwarescore=0 spamscore=0 mlxlogscore=999 phishscore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2009150000 definitions=main-2103250071 X-Mailman-Approved-At: Thu, 25 Mar 2021 08:28:45 -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-Virus-Version: vendor=baseguard engine=ICAP:2.0.136,Aquarius:18.0.761,Hydra:6.0.369,FMLib:17.0.607.475 definitions=2021-03-25_03,2021-03-24_02,2020-04-07_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 adultscore=0 priorityscore=1501 lowpriorityscore=0 bulkscore=0 mlxlogscore=999 impostorscore=0 phishscore=0 spamscore=0 clxscore=1011 malwarescore=0 mlxscore=0 suspectscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2009150000 definitions=main-2103250093 Xref: news.gmane.io gmane.comp.science.types.announce:9528 gmane.comp.lang.agda:12536 gmane.science.mathematics.categories:10429 gmane.science.mathematics.prooftheory:1653 Archived-At: --===============5531847131521640766== 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 ] --===============5531847131521640766== Content-Type: multipart/alternative; boundary="0000000000004d82f505be58de05" --0000000000004d82f505be58de05 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 2021 - 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 --0000000000004d82f505be58de05 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

ITRS 2021 Call for papers

Tenth Workshop on Intersection Type= s and Related Systems - ITRS 2021

17 July 2021= , Online

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

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

Aims and Scope

Intersecti= on types were introduced near the end of the 1970s to overcome the limitati= ons 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 such that a term of= type t =E2=88=A7 s can be used at both type t and s within the same contex= t. This provides a finite polymorphism where various, even unrelated, types= of the term are listed explicitly, differently from the more widely used u= niversally 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 polymo= rphism.

Although intersection types were initia= lly intended for use in analyzing and/or synthesizing lambda models as well= as in analyzing normalization properties, over the last twenty years the s= cope of the research on intersection types and related systems has broadene= d in many directions. Restricted (and more manageable) forms have been inve= stigated, such as refinement types. Type systems based on intersection type= theory have been extensively studied for practical purposes, such as progr= am analysis and higher-order model checking. The dual notion of union types= turned out to be quite useful for programming languages. Finally, the beha= vioural approach to types, which can give a static specification of computa= tional properties, has become central in the most recent research on type t= heory.

The ITRS 2021 workshop aims to bring tog= ether 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:

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

Invite= d Speaker

  • Jeremy Siek (Indiana University Bloomington)

Paper Submissions

Papers must be original and= not previously published, nor submitted elsewhere. Papers should be prepar= ed in LaTeX using the=C2=A0EPTCS macro=C2=A0package and shou= ld be in the range of 3-16 pages, plus at most 2 pages of references. Submi= ssions will be collected via EasyChair and reviewed by anonymous referees.<= /p>

Important Dates

  • Paper submission: 12 April 2021
  • Author notification: 24 May 2021
  • Final version: 18 June 2021
  • Workshop: 17 J= uly 2021

Program Committee

  • Antonio Bucciarelli, Univ= ersit=C3=A9 de Paris, France
  • Daniel De Carvalh= o, Innopolis University, Russia
  • Andrej Dudenhe= fner, Saarland University, Germany
  • Silvia Ghil= ezan, University of Novi Sad, Serbia
  • Giulio Gu= errieri, University of Bath, UK
  • Ugo de' Li= guoro, Universit=C3=A0 di Torino, Italy (chair)
  • Jeremy Siek, Indiana University Bloomington, USA (co-chair)

Organizers

Ugo de' Liguoro, Univ= ersit=C3=A0 di Torino, Italy

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

Steer= ing Committee

  • Mariangiola Dezani-Ciancaglini, Universit=C3=A0 di Torino, = Italy
  • Jakob Rehof, TU University of Dortmund, = Germany
  • Joe Wells, Heriot-Watt University, Sco= tland

--0000000000004d82f505be58de05-- --===============5531847131521640766==--