From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10088 Path: news.gmane.org!.POSTED.blaine.gmane.org!not-for-mail From: Riccardo Treglia Newsgroups: gmane.comp.science.types.announce,gmane.science.mathematics.logic.coq.club,gmane.comp.lang.agda,gmane.science.mathematics.categories Subject: ITRS 2020: FInal Call for Papers (Due on 10 Jan, 2020) Date: Fri, 3 Jan 2020 12:00:09 +0100 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============9214194897172303345==" Injection-Info: blaine.gmane.org; posting-host="blaine.gmane.org:195.159.176.226"; logging-data="77808"; mail-complaints-to="usenet@blaine.gmane.org" Cc: "Ugo De' Liguoro" To: eutypes-Mttm5w9jbbk@public.gmane.org, coq-club-MZpvjPyXg2s@public.gmane.org, agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org, types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org Original-X-From: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Sat Jan 04 16:44:08 2020 Return-path: Envelope-to: gcst-types-announce-Uylq5CNFT+jYtjvyW6yDsg@public.gmane.org Original-Received: from rhizome.seas.upenn.edu ([158.130.69.24]) by blaine.gmane.org with esmtp (Exim 4.89) (envelope-from ) id 1inlar-000JyD-Il; Sat, 04 Jan 2020 16:44:02 +0100 Original-Received: from RHIZOME.SEAS.UPENN.EDU (localhost.upenn.edu [127.0.0.1]) by RHIZOME.seas.upenn.edu (8.15.2/8.14.3) with ESMTP id 004FgMLd011023; Sat, 4 Jan 2020 10:42:28 -0500 X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $ Original-Received: from psychopathy.seas.upenn.edu (psychopathy.seas.upenn.edu [158.130.67.191]) by RHIZOME.seas.upenn.edu (8.15.2/8.14.3) with ESMTP id 003B0kOk017581 for ; Fri, 3 Jan 2020 06:00:46 -0500 Original-Received: from mx0b-000c2a01.pphosted.com (mx0b-000c2a01.pphosted.com [148.163.155.36]) by psychopathy.seas.upenn.edu (8.15.2/8.15.2) with ESMTPS id 003B0k1b043197 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Fri, 3 Jan 2020 06:00:46 -0500 Original-Received: from pps.filterd (m0128480.ppops.net [127.0.0.1]) by mx0b-000c2a01.pphosted.com (8.16.0.42/8.16.0.42) with SMTP id 003Av8sQ018122 for ; Fri, 3 Jan 2020 06:00:46 -0500 Authentication-Results: ppops.net; spf=pass smtp.mailfrom=riccardo.treglia-Ob+gDNbliO0@public.gmane.org Original-Received: from mail-wm1-f68.google.com (mail-wm1-f68.google.com [209.85.128.68]) by mx0b-000c2a01.pphosted.com with ESMTP id 2x6261br5f-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NOT) for ; Fri, 03 Jan 2020 06:00:46 -0500 Original-Received: by mail-wm1-f68.google.com with SMTP id p17so8233618wma.1 for ; Fri, 03 Jan 2020 03:00:45 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=unito.it; s=google; h=mime-version:from:date:message-id:subject:to:cc; bh=tkNJho9IhSuX81epDs2binm1TmzXM61IkNdpxY2Np5c=; b=GrO9gQUTat4prRJHHq94ZYeKqE1oNS9i53RQ4+DFVfSNDxGe1jBBdanZKjHdxQcMDY 87VUYGy1Y3AX2nkSH++e4lIA9HKYEcGQ6/tLuf3v3MRhwghd36i00NMIzn4zAlJ7P/Oo qb9PXYzZX2+SA8EpHEqR6EmBa/V/SuhaOLZVA= 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:cc; bh=tkNJho9IhSuX81epDs2binm1TmzXM61IkNdpxY2Np5c=; b=KzT5tv5g06MU+9gUhn3N/8q0lZ8n2d3hjmF5T/dPGopS+F7po/wrzY20qQtSBxYizE CmF1SIpmwf8NaoZHYywOW/faYmKXUvr98uBHI6Bpl3N4KXgT01ElBW+Qk18ERkB8U/Ql O0v+D8EomLxBSmGxVxGMMZB2nQQynV8qr6tmjg4ZSb53efy4sz6ahn0PtbZsO0CMJI4H 91G9N40j3/4K9V0tntYcJxot3lqHH5MQ5AUBkxWej+fbPAIG8NXv5QH7vHjU49zulLhm NtwB+gvva9UKg86cJ2Rxvtn6PvjU0c0xag4W7PQGGZ0/pduEC2NnYMmpV0GIYh3+K29a BIBQ== X-Gm-Message-State: APjAAAV5HmZXN9lh+sxtEa7DFC1NqMMTpSVY4qrV0GAcgxuW1kdmsy7P n9isy/5sU2fKdYQbshcsnvS9h4iGZ8hyEJZwfa9Gag== X-Google-Smtp-Source: APXvYqygqW7vwKqrXF6qscc2Mc6og8YL56ESj1r7v9G2DhBXyn2zdzYGw3a5PvzZKlxjqqX+7U9F3SS2UOv/Kv+JYKU= X-Received: by 2002:a05:600c:20c7:: with SMTP id y7mr19692120wmm.21.1578049244267; Fri, 03 Jan 2020 03:00:44 -0800 (PST) X-CLX-Shades: MLX X-CLX-Response: 1TFkXGRoTEQpMehcaEQpZRBdlY2FyY2xkXBNATREKWFgXYW56GEZSZ21nXh0 RCnhOF21/aEtAQWRgZFBrEQp5TBdpYUccHWNdcmVyQxEKeUMXYUllHl1NHBpNRAERCkNIFwcZHB IRCkNZFwcbGR4RCkNJFxoEGhoaEQpZTRdnZnIRCllJFxpxGwYadwYYGhoGGRpCHAYaBh0TBhpxG hAadwYaBhoGGgYaBhoGGnEaEBp3BhoRClleF2hueREKSUYXX1pPRERZT0tZdUJFWV5PThEKQ04X H0FYXXxPcE9SXmFgGUx7ZF9NfVIZbXhDUF9JYRtTTW8RClhcFx8EGgQbExsHTBkZTk4bHkkFGxo EGxsaBB8aBBseHxAbHhofGhEKXlkXfHhnZB8RCk1cFxsfExEKTFoXaGlNa2sRCkJPF2h9QWBDWn 1zR0ETEQpDWhcYGhMEEh8EGxgSBBwSEQpCXhcbEQpEXhcfEQpESRcbEQpCXBcaEQpCRRdvHmdTR GR/QR9lBREKQk4XbX9oS0BBZGBkUGsRCkJMF2FuehhGUmdtZ14dEQpCbBdmG0NcHWBuHhxseBEK QkAXaVBYcl9yaBxTR1kRCkJYF29ER096fF1MW0xoEQpNXhcHGxEKWlgXGREKcGgXZlBZTmRneE9 OAUQQBxkaEQpwaBdoGHhpbxtCYW8cUxAHGRoRCnBoF2wcQWZfXWdbH0RNEAcZGhEKcGgXbWZaSG dzflhscgEQBxkaEQpwaBdrZlhQSURFRXgfUBAHGRoRCnB9F2taaHBvWGB7QGJBEAcZGhEKcH8XZ kF/fG59HWVeHkIQBxkaEQpwXxdgQhNwf0JtZB9JfBAHGRoRCnBsF X-Proofpoint-SPF-Result: pass X-Proofpoint-SPF-Record: v=spf1 ip4:130.192.119.34 ip4:130.186.3.0/24 ip4:130.186.31.160/27 ip4:130.186.7.110 include:spf.mailjet.com include:spf.mandrillapp.com include:_spf.cineca.it include:_spf.google.com ~all] X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.95,18.0.572 definitions=2020-01-03_02:2020-01-02,2020-01-03 signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 suspectscore=0 phishscore=0 bulkscore=0 adultscore=0 spamscore=0 priorityscore=0 lowpriorityscore=0 clxscore=309 mlxlogscore=999 mlxscore=0 malwarescore=0 impostorscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-1910280000 definitions=main-2001030103 X-Mailman-Approved-At: Sat, 04 Jan 2020 10:35:37 -0500 X-BeenThere: types-announce-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org X-Mailman-Version: 2.1.29 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" Xref: news.gmane.org gmane.comp.science.types.announce:8837 gmane.science.mathematics.logic.coq.club:22874 gmane.comp.lang.agda:11443 gmane.science.mathematics.categories:10088 Archived-At: --===============9214194897172303345== 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 ] --===============9214194897172303345== Content-Type: multipart/alternative; boundary="000000000000a49f80059b3a3802" --000000000000a49f80059b3a3802 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable ITRS 2020 Call for contributions Tenth Workshop on Intersection Types and Related Systems 6 March 2020, Turin Affiliated with Types 2020 https://types2020.di.unito.it/itrs.html 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 which 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 2020 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; Information about the previous events is available at the ITRS home page. Paper Submissions Authors are invited to submit an abstract (2 pages bibliography excluded) in PDF format, through EasyChair. Publishing of a full paper is planned in post-proceedings to appear in EPTCS, therefore we recommend using the EPTCS macro package to prepare submissions. Informal proceedings will be made available at the workshop. Invited Speaker Jeremy Siek (Indiana University Bloomington) Important Dates Abstract submission: 10 January, 2020 Author notification: 1 February, 2020 Final version: 15 February, 2020 Workshop: 6 March, 2020 Program Committee Ugo de' Liguoro (University of Turin) Jeremy Siek (Indiana University Bloomington) Andrej Dudenhefner (Saarland University) Antonio Bucciarelli (Universit=C3=A9 Paris Diderot) Daniel de Carvalho (Innopolis University) Kazushige Terui (Kyoto University) Silvia Ghilezan (University of Novi Sad) Organizers Ugo de' Liguoro (University of Turin, Italy) Riccardo Treglia (University of Turin, Italy) Steering Committee Mariangiola Dezani-Ciancaglini (University of Turin, Italy) Jakob Rehof (University of Dortmund, Germany) Joe Wells (Heriot-Watt University, Scotland) --000000000000a49f80059b3a3802 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

ITRS 2020 Call for contributions


Tenth Workshop on Inter= section Types and Related Systems

6 March 2020, Turin

Affiliated with T= ypes 2020


https:/= /types2020.di.unito.it/itrs.html


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 = which 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 initially intended for use i= n analyzing and/or synthesizing lambda models as well as in analyzing norma= lization properties, over the last twenty years the scope of the research o= n intersection types and related systems has broadened in many directions. = Restricted (and more manageable) forms have been investigated, such as refi= nement types. Type systems based on intersection type theory have been exte= nsively studied for practical purposes, such as program analysis and higher= -order model checking. The dual notion of union types turned out to be quit= e useful for programming languages. Finally, the behavioural approach to ty= pes, which can give a static specification of computational properties, has= become central in the most recent research on type theory.


<= p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0pt;margin-bottom:0pt"><= span style=3D"font-size:11pt;font-family:"Courier New";color:rgb(= 0,0,0);background-color:transparent;font-variant-numeric:normal;font-varian= t-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The ITRS = 2020 workshop aims to bring together researchers working on both the theory= and practical applications of systems based on intersection types and rela= ted approaches. Possible topics for submitted papers include, but are not l= imited 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 s= ystems.

  • Applications for pro= gramming languages, program analysis, and program verification.

    <= /li>

  • Applications for other areas, such as d= atabase query languages and program extraction from proofs.

    • =

  • Related approaches using behavioural/intens= ional types and/or denotational semantics to characterize computational pro= perties.

  • Quantitative refine= ments of intersection types.


ITRS workshops have been hel= d every two years; Information about the previous events is available at th= e ITRS home page.


Paper Submissions


Authors are invited to subm= it an abstract (2 pages bibliography excluded) in PDF format, through EasyC= hair. Publishing of a full paper is planned in post-proceedings to appear i= n EPTCS, therefore we recommend using the EPTCS macro package to prepare su= bmissions. Informal proceedings will be made available at the workshop.


Invited Speaker


Jeremy Siek (Indiana University B= loomington)


Important Dates


Abstract submission: 10 January, 2020=

Auth= or notification: = 1 February, 2020

Final version: =C2=A0 =C2=A0 =C2=A0 =C2=A0 15 February, 202= 0

Workshop: =C2=A0 =C2=A0 6 March, 2020


Program Committee

Ug= o de' Liguoro (University of Turin)

Jeremy Siek=C2=A0 (Indiana Univer= sity Bloomington)

Andrej Dudenhefner (Saarland University)

Antonio Bucc= iarelli (Universit=C3=A9 Paris Diderot)

Daniel de Carvalho (Innopolis Uni= versity)

Kazushige Terui (Kyoto University)

Silvia Ghilezan (University= of Novi Sad)


Organizers

Ugo de' Liguoro (University of Turin, = Italy)

Riccardo Treglia (University of Turin, Italy)


Steering Commi= ttee


Mariangiola Dezani-Ciancaglini (University of Turin, Italy)

Ja= kob Rehof (University of Dortmund, Germany)

Joe Wells (Heriot-Watt Unive= rsity, Scotland)=C2=A0


--000000000000a49f80059b3a3802-- --===============9214194897172303345==--