From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10560 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: Tue, 21 Sep 2021 11:31:14 +0200 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============8391053256145608509==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="607"; 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 Tue Sep 21 11:49:41 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 1mScPF-000ASR-8W for gcst-types-announce@m.gmane-mx.org; Tue, 21 Sep 2021 11:49:41 +0200 Original-Received: from pps.filterd (m0172791.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.16.1.2/8.16.1.2) with SMTP id 18L8xUMC026664; Tue, 21 Sep 2021 05:47:19 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0a-00390e01.pphosted.com with ESMTP id 3b6w3n2w0w-1; Tue, 21 Sep 2021 05:47:19 -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 18L9l8H2037828; Tue, 21 Sep 2021 05:47:09 -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 18L9l8eR090303; Tue, 21 Sep 2021 05:47:08 -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 18L9VWf5088920 for ; Tue, 21 Sep 2021 05:31:33 -0400 Original-Received: from pps.filterd (m0172794.ppops.net [127.0.0.1]) by mx0b-00390e01.pphosted.com (8.16.1.2/8.16.1.2) with SMTP id 18L8k8Xd010139 for ; Tue, 21 Sep 2021 05:31:32 -0400 Original-Received: from mail-il1-f181.google.com (mail-il1-f181.google.com [209.85.166.181]) by mx0b-00390e01.pphosted.com with ESMTP id 3b5wcf8myb-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Tue, 21 Sep 2021 05:31:32 -0400 Original-Received: by mail-il1-f181.google.com with SMTP id b6so21959946ilv.0 for ; Tue, 21 Sep 2021 02:31:32 -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=bNSSG+GjBL/uLXvt0UonAMwTwmBUITaL3o+d1l7fOLc=; b=TVM+BgU7Jgp0u2/MhyGvNkbh3n599jCwRpM7KgZ4MSn1EwpP3lbVpJxhdLneRdZdsX CfEgfprKe2eHVDcZJlt7S371SDW+uw4W/ocku78UMcRs3u3gtTFJnkkJeBA+/jrYKWWj EfzvYKJdGVzGnw5EBs17pCaF3xXAYTJobibP4= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=bNSSG+GjBL/uLXvt0UonAMwTwmBUITaL3o+d1l7fOLc=; b=X3QuBj2nhgJzgFEMmYeXVzPHrnTe2ldHRAd9+Ye9rT78llj9FLRxLOQPCnf087jahs x8s5aPUyZjCoTluoKS9+WywuIpMZaJ0rQlRCQb+W8lqFMaDbIhdro3aWNCjSyI121ZUC 9qYtmXsDi06RI63Nzl1x87CdJJfOas4Awb941QJ2jQgU5JSdj79lMvfX+XRxBSkapY/1 3Jj+/9RPtXzcIatduZmny4zgtoYk8iN0A+8Wm9CpY588Rcny23vg6FORixx754YTTwsL 7/srB6W1Ew4HfZUhLc2snmC0BGj9QkGXB/m6q8VMhuY4DECzClzwAWwdWPJkf+Vsr2RR e3rA== X-Gm-Message-State: AOAM531AA3w3wB3rb9P3YttzPkpz7s/fY9k4/4c6piOPZ59Q0VXJARJN Po4kw/8AUiq8l26EWgP4sxHIq0ehUfAyyY/zl6qVcTK51F0Hvw== X-Google-Smtp-Source: ABdhPJzc/x0EjJfhFd8P1FIabNiNiySEssMiTbAlJh4Y7i1Yt4Ham9ivDHiGSf28EwgANPkmUjIirvB0yRW4f78iCvM= X-Received: by 2002:a05:6e02:1caa:: with SMTP id x10mr20387509ill.280.1632216691544; Tue, 21 Sep 2021 02:31:31 -0700 (PDT) X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.182.1,Aquarius:18.0.790,Hydra:6.0.391,FMLib:17.0.607.475 definitions=2021-09-21_01,2021-09-20_01,2020-04-07_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 malwarescore=0 lowpriorityscore=0 impostorscore=0 bulkscore=0 mlxscore=0 priorityscore=0 suspectscore=0 phishscore=0 mlxlogscore=878 spamscore=0 adultscore=0 clxscore=68 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2109030001 definitions=main-2109210060 X-Mailman-Approved-At: Tue, 21 Sep 2021 05:47:07 -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: tIjroz_2hb48wnUEocZ9kC0q3JyqcDkA X-Proofpoint-ORIG-GUID: tIjroz_2hb48wnUEocZ9kC0q3JyqcDkA X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.182.1,Aquarius:18.0.790,Hydra:6.0.391,FMLib:17.0.607.475 definitions=2021-09-21_01,2021-09-20_01,2020-04-07_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 suspectscore=0 adultscore=0 impostorscore=0 phishscore=0 spamscore=0 mlxlogscore=999 clxscore=1011 malwarescore=0 priorityscore=1501 bulkscore=0 mlxscore=0 lowpriorityscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2109030001 definitions=main-2109210062 Xref: news.gmane.io gmane.comp.science.types.announce:9854 gmane.comp.lang.agda:12737 gmane.science.mathematics.categories:10560 gmane.science.mathematics.prooftheory:1669 Archived-At: --===============8391053256145608509== 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 ] --===============8391053256145608509== Content-Type: multipart/alternative; boundary="00000000000018abe605cc7e1012" --00000000000018abe605cc7e1012 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!FLn7aHMzY6HrXO3KJJA59O83OnWqksX9LvNZresHtiVy7ClLtbwjipgIX= qebOfIjGgo_N6dpZd2c0Q$=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) --00000000000018abe605cc7e1012 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable

ITRS 2021 Call for Post-Proceedings

Tenth Workshop on Interse= ction Types and Related Systems - ITRS 2021

17= July 2021, Online

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

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

Aims and Scope

Intersection types were introduced near the end of the 197= 0s 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 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 v= arious, even unrelated, types of the term are listed explicitly, differentl= y from the more widely used universally quantified types where the polymorp= hic type is the common schema that stands for its various type instances. A= s a consequence, more terms (all and only the normalizing terms) can be typ= ed than with universal polymorphism.

Although i= ntersection types were initially intended for use in analyzing and/or synth= esizing lambda models as well as in analyzing normalization properties, ove= r the last twenty years the scope of the research on intersection types and= related systems has broadened in many directions. Restricted (and more man= ageable) forms have been investigated, such as refinement types. Type syste= ms based on intersection type theory have been extensively studied for prac= tical purposes, such as program analysis and higher-order model checking. T= he dual notion of union types turned out to be quite useful for programming= languages. Finally, the behavioral approach to types, which can give a sta= tic specification of computational properties, has become central in the mo= st recent research on type theory.

The ITRS 202= 1 workshop aims to bring together researchers working on both the theory an= d practical applications of systems based on intersection types and related= approaches. Possible topics for submitted papers include, but are not limi= ted to:

  • Formal properties of systems with intersection types.
  • Results for related systems, such as union types, refinement t= ypes, or singleton types.
  • Applications to lamb= da calculus, pi-calculus and similar systems.
  • = Applications for programming languages, program analysis, and program verif= ication.
  • Applications for other areas, such as= database query languages and program extraction from proofs.
  • Related approaches using behavioral/intensional types and/o= r 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 abou= t the previous events is available on the=C2=A0ITRS home page.

    Post-Proc= eedings

    We are planning post-proceedings, incl= uding presentations to the workshop and submissions accepted via an open ca= ll with=C2=A0dates:

    • submission deadline:=C2=A01 October
    • accepta= nce communication:=C2=A05 November
    • camera-ready version:=C2=A019 November

    Pape= rs should not be published elsewhere, with original results or surveying on= going research. They should be written in English using LaTex and will appe= ar on EPTCS: see=C2=A0Information for Authors. Submissions should be 20 pages long, excludi= ng bibliography and avoiding technical 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 Dezani-Ciancaglini, Un= iversit=C3=A0 di Torino, Italy
  • Jakob Rehof, TU= University of Dortmund, Germany
  • Joe Wells, He= riot-Watt University, Scotland

Organizers:

--00000000000018abe605cc7e1012-- --===============8391053256145608509==--