From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10445 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 (Extended Deadline) Date: Fri, 9 Apr 2021 11:31:28 +0200 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============2781415170829979379==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="2936"; 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 Fri Apr 09 13:01:16 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 1lUot1-0000YG-Ks for gcst-types-announce@m.gmane-mx.org; Fri, 09 Apr 2021 13:01:15 +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 139Au3fU032119; Fri, 9 Apr 2021 07:00:21 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0b-000c2a01.pphosted.com with ESMTP id 37sxa58bt0-1; Fri, 09 Apr 2021 07:00:21 -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 139B08J4073386; Fri, 9 Apr 2021 07:00:08 -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 139B08de083857; Fri, 9 Apr 2021 07:00:08 -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 1399W1aG068894 for ; Fri, 9 Apr 2021 05:32:02 -0400 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 1399RLWE019928 for ; Fri, 9 Apr 2021 05:32:01 -0400 Original-Received: from mail-ej1-f43.google.com (mail-ej1-f43.google.com [209.85.218.43]) by mx0a-00390e01.pphosted.com with ESMTP id 37rvc0nk64-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Fri, 09 Apr 2021 05:32:01 -0400 Original-Received: by mail-ej1-f43.google.com with SMTP id e14so7578856ejz.11 for ; Fri, 09 Apr 2021 02:32:00 -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=xkvs9mTg2Pr1eiHVVULgMVf7h3dtfmpN53C/lvZFcEA=; b=NV5Bb8U2nhZJogLuhuAxO5J23LoszyWWHsLZE+YbkpiCsrHcb3lV5I3cwMs4GYeNrX CCDVQFN0NPiBcfit6nX2ePAJ9PQVKRYXB1AdOFd2/ZrFtHt2k2ACkOvoThwAWr4KVgr1 aYkHTlNRA+wSOGLJw0v7Nzvvrz2g+zGk15xnc= 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=xkvs9mTg2Pr1eiHVVULgMVf7h3dtfmpN53C/lvZFcEA=; b=XQHKc+LKNZykeYtra7whNF+0nXfj3GgH3Xejtd8zT1Hwf55rAV/ryAZypZqeylrW2u 6G7FsNuLAkkFt5svo2M/oBAUJgG4b6OQ/q22uHFZVD4zgtIo5IE9cJO8CURzqgNBC7RQ RCbmYRKwVPtObCpTvoveXwysqEuDPgsjPKuqr40xkYSbrCs1gQAW6f8ryYHECdWEEJRs fHMy/8Ta6111qQ1PdF0i5squCsB/LPqxkTFxbjMYHcnwSJKP2W7VJOGFY1XTN/wd44fA vTqCw80r1IQJtqS5/nEEAfgSsq0oOr1hXolJdAbzqfnDuvn1jyhR0AB6hGConaS54vXQ Hp9Q== X-Gm-Message-State: AOAM532D/rCrWl/4ZaIOt+opgQw5cTSDMBgihdQjZB9vwDg87S8XL+Gx RUPch0G8Pk6t2+Pwi4JL4IkWCCxids1bwpzVyveqvg== X-Google-Smtp-Source: ABdhPJzZk7NsqkvO61jW9c2K1lUV8RSm7GMf30GGyDKmomjjYysEPzH9qoBjESXQk3fNiuZn9h+ObtaBiFmQExMoW0s= X-Received: by 2002:a17:907:c16:: with SMTP id ga22mr15108810ejc.120.1617960719077; Fri, 09 Apr 2021 02:31:59 -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-09_05:2021-04-09, 2021-04-09 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 impostorscore=0 priorityscore=48 spamscore=0 suspectscore=0 phishscore=0 adultscore=0 bulkscore=0 mlxlogscore=999 malwarescore=0 clxscore=304 mlxscore=0 lowpriorityscore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2104060000 definitions=main-2104090068 X-Mailman-Approved-At: Fri, 09 Apr 2021 06:59:59 -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: aIU_adW6hn-kSK34QZXmAV2iwLxIvROj X-Proofpoint-ORIG-GUID: aIU_adW6hn-kSK34QZXmAV2iwLxIvROj 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-09_05,2021-04-09_01,2020-04-07_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 clxscore=1011 mlxlogscore=999 adultscore=0 impostorscore=0 suspectscore=0 mlxscore=0 bulkscore=0 priorityscore=1501 lowpriorityscore=0 malwarescore=0 spamscore=0 phishscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2104060000 definitions=main-2104090080 Xref: news.gmane.io gmane.comp.science.types.announce:9558 gmane.comp.lang.agda:12546 gmane.science.mathematics.categories:10445 gmane.science.mathematics.prooftheory:1654 Archived-At: --===============2781415170829979379== 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 ] --===============2781415170829979379== Content-Type: multipart/alternative; boundary="000000000000ebe52405bf86d5fb" --000000000000ebe52405bf86d5fb 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 --000000000000ebe52405bf86d5fb 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= =A0= FSCD, 17-24 July 2021, Buenos Aires

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

Aims and Scope

Intersectio= n types were introduced near the end of the 1970s to overcome the limitatio= ns of Curry's type assignment system and to provide a characterization = of the strongly normalizing terms of the Lambda Calculus. The key idea is t= o 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 provides a finite polymorphism where various, even unrelated, types = of the term are listed explicitly, differently from the more widely used un= iversally quantified types where the polymorphic type is the common schema = that stands for its various type instances. As a consequence, more terms (a= ll and only the normalizing terms) can be typed than with universal polymor= phism.

Altho= ugh 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 type= s and related systems has broadened in many directions. Restricted (and mor= e 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 checki= ng. The dual notion of union types turned out to be quite useful for progra= mming 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 system= s based on intersection types and related approaches. Possible topics for s= ubmitted papers include, but are not limited to:

  • Formal properties of systems with intersection types.
  • Results for related systems, such as union types, refinemen= t types, or singleton types.
  • Applications to l= ambda calculus, pi-calculus and similar systems.
  • Applications for programming languages, program analysis, and program ve= rification.
  • Applications for other areas, such= as database query languages and program extraction from proofs.
  • Related approaches using behavioural/intensional types a= nd/or denotational semantics to characterize computational properties.
    • =
  • Quantitative refinements of intersection types.

ITRS wor= kshops have been held every two years (with the exception of 2020, because = of COVID-19 outbreak). Information about the previous events is available o= n the=C2=A0ITRS home page.

Invited Speaker

  • Jeremy Siek (Indiana University Bloomin= gton)

Paper Submissions

Papers must be orig= inal and not previously published, nor submitted elsewhere. Papers should b= e prepared in LaTeX using the=C2=A0EPTCS macro=C2=A0package and should be in t= he range of 3-16 pages, plus at most 2 pages of references. Submissions wil= l be collected via EasyChair and reviewed by anonymous referees.

Important Dates=

  • Paper submission:=C2=A012 April=C2=A026= 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-cha= ir)

Organizers:

Ugo de' Liguoro, Univer= sit=C3=A0 di Torino, Italy

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

Steering Co= mmittee

  • Mariangiola Dezani-Ciancaglini, Universit=C3=A0 di Torino, Ital= y
  • Jakob Rehof, TU University of Dortmund, Germ= any
  • Joe Wells, Heriot-Watt University, Scotlan= d

--000000000000ebe52405bf86d5fb-- --===============2781415170829979379==--