From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10538 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 2021 Call for Post-Proceedings Date: Tue, 27 Jul 2021 13:23:14 +0200 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============5597186505996987909==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="7047"; 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 Jul 27 14:17:47 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 1m8M1q-0001a5-UF for gcst-types-announce@m.gmane-mx.org; Tue, 27 Jul 2021 14:17:47 +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 16RCBf56005399; Tue, 27 Jul 2021 08:16:53 -0400 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0a-00390e01.pphosted.com with ESMTP id 3a235f6qkh-1; Tue, 27 Jul 2021 08:16:52 -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 16RCGfFm002971; Tue, 27 Jul 2021 08:16: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 16RCGfon095464; Tue, 27 Jul 2021 08:16: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 16RBNpPo089564 for ; Tue, 27 Jul 2021 07:23:52 -0400 Original-Received: from pps.filterd (m0172793.ppops.net [127.0.0.1]) by mx0b-00390e01.pphosted.com (8.16.0.43/8.16.0.43) with SMTP id 16RBHHWL022398 for ; Tue, 27 Jul 2021 07:23:51 -0400 Original-Received: from mail-ed1-f45.google.com (mail-ed1-f45.google.com [209.85.208.45]) by mx0b-00390e01.pphosted.com with ESMTP id 3a235568n3-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Tue, 27 Jul 2021 07:23:50 -0400 Original-Received: by mail-ed1-f45.google.com with SMTP id x14so10046883edr.12 for ; Tue, 27 Jul 2021 04:23:50 -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=+52nfFp49qKbDnRFMB1IYJBmK/Hu0qSb0bufSWEtexo=; b=MevXNNtwAjW8+A/JscH0tvwjrUl/VN5EmeKdBklY3a8mllMBuj9mkQnFlGWMlHn8IL VK5eWfD19XFW5a+y9/BZZPYkqXYjp0mRN+GsI8LkRr1N0d7tiMmCbBmW/WlbeLjf0nnA ThDvM6MwZYWEKsrJE3B50dArOkkxwxdotHpe0= 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=+52nfFp49qKbDnRFMB1IYJBmK/Hu0qSb0bufSWEtexo=; b=ruExuMRj4+g4kzY02Z1FXjMVEPeA8+ZUm1lhoKFCqQcBQXarj+/aCgwlBo0er8HO4Z OGwhXSBEvP8wHiDU8itT81JBlseFDPbjyFmJ6yygHOH4UDXVyc0cCyOhGiR218Q/rT9G t63eq7ZVljbtGhdfJYIyOeM/88TlPsugUgbTHZEoH4P9vaGoW9KFD4Z8n51HaQAx2Pks I+mcrZCKpNGmUbZZKKv4t+7CNue5AlyhcvSVYBxaNf0fHwsRH2483O9urDYIZcmHEE4J p5QfwLT8jEd2EUABsn/QuyvIn5isCsD2GYugqPRllK70myuFupTrfvkqpANdpPoBADPB WFVw== X-Gm-Message-State: AOAM533QrXq7DTMHfNegXn96CPRcB6FJuhLLiIPsBRXOMNhDYHyV1Yok Bz4jjNExi6G1t4Rk5yYtEMNWqWNV/tG2EGATzsCUfg== X-Google-Smtp-Source: ABdhPJwW/WGLTp67ZOEsDafb72UedCeGAttfxOEgJpIvK3/T97sv2Wxr9B5Ze/aCZuqEW2iTFrl5b78DgifCyMANsGo= X-Received: by 2002:aa7:cdcc:: with SMTP id h12mr14306455edw.39.1627385029331; Tue, 27 Jul 2021 04:23:49 -0700 (PDT) X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391, 18.0.790 definitions=2021-07-27_07:2021-07-27, 2021-07-27 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 mlxlogscore=913 clxscore=408 suspectscore=0 phishscore=0 mlxscore=0 bulkscore=0 spamscore=0 impostorscore=0 lowpriorityscore=0 priorityscore=0 adultscore=0 malwarescore=0 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2107140000 definitions=main-2107270066 X-Mailman-Approved-At: Tue, 27 Jul 2021 08:16: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: lQEw6nwkj_ynQIxttMRtWrwytCMrbB63 X-Proofpoint-ORIG-GUID: lQEw6nwkj_ynQIxttMRtWrwytCMrbB63 X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391,18.0.790 definitions=2021-07-27_07:2021-07-27,2021-07-27 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 phishscore=0 priorityscore=1501 mlxlogscore=999 clxscore=1011 adultscore=0 spamscore=0 bulkscore=0 suspectscore=0 lowpriorityscore=0 impostorscore=0 mlxscore=0 malwarescore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2107140000 definitions=main-2107270072 Xref: news.gmane.io gmane.comp.science.types.announce:9773 gmane.comp.lang.agda:12700 gmane.science.mathematics.categories:10538 gmane.science.mathematics.prooftheory:1665 Archived-At: --===============5597186505996987909== 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 ] --===============5597186505996987909== Content-Type: multipart/alternative; boundary="0000000000009620d005c8191a2a" --0000000000009620d005c8191a2a 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: 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 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 . Submissions 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) --0000000000009620d005c8191a2a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

ITRS 2021 Call for Post-Proceedings

Tenth Workshop on Intersection Types and Related Systems - ITRS 2021

<= p style=3D"margin:15px 0px;color:rgb(0,0,0);font-family:Helvetica,arial,san= s-serif;font-size:14px">17 July 2021, Online

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

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

Aims a= nd Scope

Intersection types were introduced ne= ar the end of the 1970s to overcome the limitations of Curry's type ass= ignment system and to provide a characterization of the strongly normalizin= g terms of the Lambda Calculus. The key idea is to introduce an intersectio= n 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 p= olymorphism where various, even unrelated, types of the term are listed exp= licitly, differently from the more widely used universally quantified types= where the polymorphic type is the common schema that stands for its variou= s type instances. As a consequence, more terms (all and only the normalizin= g terms) can be typed than with universal polymorphism.

Although intersection types were initially intended for use in ana= lyzing and/or synthesizing lambda models as well as in analyzing normalizat= ion properties, over the last twenty years the scope of the research on int= ersection types and related systems has broadened in many directions. Restr= icted (and more manageable) forms have been investigated, such as refinemen= t types. Type systems based on intersection type theory have been extensive= ly studied for practical purposes, such as program analysis and higher-orde= r model checking. The dual notion of union types turned out to be quite use= ful for programming languages. Finally, the behavioural approach to types, = which can give a static specification of computational properties, has beco= me central in the most recent research on type theory.

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

ITRS workshops have been he= ld every two years (with the exception of 2020, because of COVID-19 outbrea= k). Information about the previous events is available on the=C2=A0ITRS home pag= e.

Pos= t-Proceedings

We are planning post-proceedings= , including presentations to the workshop and submissions accepted via an o= pen call with=C2=A0dates:

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

= Papers should not be published elsewhere, with original results or surveyin= g ongoing research. They should be written in English using LaTex, and will= appear on EPTCS: see=C2=A0Information for Authors. Submissions should be 20 pa= ges long, excluding bibliography and avoiding technical appendices. Submiss= ions are expected via=C2=A0EasyChair.

Program Committee

<= ul style=3D"margin:15px 0px;padding-left:30px;color:rgb(0,0,0);font-family:= Helvetica,arial,sans-serif;font-size:14px">
  • 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 (chai= r)
  • Jeremy Siek, Indiana University Bloomington= , USA (co-chair)

    • Steering Committee

    • Mariangiola Dezani-Ciancaglini, Univers= it=C3=A0 di Torino, Italy
    • Jakob Rehof, TU Univ= ersity of Dortmund, Germany
    • Joe Wells, Heriot-= Watt University, Scotland

    Organizers:

    --0000000000009620d005c8191a2a-- --===============5597186505996987909==--