Affiliated with FSCD 2024, 10-13 July 2024, Tallinn

ITRS past events: http://itrs.di.unito.it/workshops.html

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 ∧ such that a term of type t ∧ 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 2024 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.

- Andrej Dudenhefner: invited speaker of ITRS
- Viviana Bono: jointly invited spekaer of ITRS+WIL
- Giulio Manzonetto: jointly invited speaker of ITRS+TLLA

Submission should be between 3 and 5 pages, excluding bibliography. We welcome original results or surveys about ongoing research, short versions of recently published articles, papers submitted elsewhere, and surveys of ongoing work. Communications should be written in English, using LaTeX, and will appear on the workshop website.

The submission Web page for ITRS24 is on Easychair: https://easychair.org/conferences/?conf=itrs24- Paper submission:
~~May, 6th~~ - Author notification:
~~May, 22th~~ - Final version:
**June, 22th**

- Early Bird:
~~May, 17th~~ - Regular:
**June, 19th** - Official joint conferences website: LiCS ICALP FSCD 2024 (ioc.ee)
- Registration platform: ICALP_LiCS_FSCD2024 - Tickets | Fienta

- Delia Kesner - Chair (Universite Paris Cite)
- Pawel Parys (University of Warsaw)
- Paola Gianinni (Università del Piemonte Orientale)
- Silvia Ghilezan (University of Novi Sad)
- Kim Nguyen (Universite Paris Saclay)
- Pablo Barenbaum (Universidad Buenos Aires)
- Ugo de'Liguoro (Università Torino)

- 9:00 - 9:15 Welcome
- 9:15 - 10:00 Andrej Dudenhefner: From Normalization to Typability via Subject Expansion (ITRS invited talk) [pdf] [slides]

- 10:30 - 10:52 Miguel Ramos: Non-Idempotent Intersection Types for Global State [pdf] [slides]
- 10:52 - 11:14 Beniamino Accattoli, Giulio Guerrieri and Maico Leberle: Strong Call-by-Value and Multi Types [pdf] [slides] [video]
- 11:14 - 11:36 Victor Arrial: Call-by-Value Typing Revisited, for Free? [pdf] [slides][video]

- 11:45 - 12:30 Giulio Manzonetto: Coloring Intersection Types (ITRS + TLLA invited talk)

- 14:00 - 14:45 Viviana Bono: Types for (Slow) AI (ITRS + WIL invited talk)

- 16:00 - 16:22 Joseph Paulus, Daniele Nantes-Sobrinho and Jorge A. Pérez: Intersection Types Meet Session Types [pdf] [slides] [video]
- 16:22 - 16:44 Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro and Betti Venneri:

YACC: Yet Another Church Calculus [pdf] [slides] [video]

- 16:49 - 17:11 Pablo Barenbaum, Eduardo Bonelli and Mariana Milicich: Intersection Types as Evaluation Types [pdf] [slides] [video]
- 17:11 - 17:34 Aleksy Schubert: Modest annotations with intersection types [pdf] [slides]
- 17:34 - 17:57 Abhishek De, Charles Grellois, Lê Thành Dũng Nguyễn and Cécilia Pradic:

Higher-order model checking meets implicit automata: Finitary colored semantics of infinitary λ-terms [pdf] [slides]

**Andrej Dudenhefner: From Normalization to Typability via Subject Expansion.**
In the early 1980s Coppo and Dezani-Ciancaglini presented an intersection type assignment system (CD) as an extension
of the simple type system. In their seminal work, CD is shown to assign types to strongly normalizing terms
in the λ-I-calculus. Afterwards, Pottinger has shown that any strongly normalizing term is typable in CD.
As keenly remarked by Barendregt, Dekkers, and Statman, there are many proofs of this fact in literature,
most of which (including Pottinger’s) are incorrect.

The present work gives an alternative approach to show that strongly normalizing terms are typable in CD.
The key idea is to use a recently developed notion of IK′-reduction, which allows for subject expansion properties.
Any strongly normalizing term M reduces to a typable normal form via the IK′-reduction. Therefore,
subject expansion properties imply typability of M. In order to eliminate any doubt, the proof is mechanized
in constructive logic using the Coq proof assistant.

**Giulio Manzonetto: Coloring Intersection Types.**
We review the key findings on intersection type systems by
comparing two main approaches: the qualitative analysis of termination
properties and the quantitative evaluation of resource consumption. We
will expose the relationship between the underlying systems of
approximants, based on Böhm trees and Taylor expansions, and
observational equivalences. We will then introduce the "yinyang
calculus", an annotated lambda-calculus that allows to track the
interaction between a lambda-term and its environment. By
appropriately coloring an intersection type system, we prove that the
usual Böhm tree equality can be characterized in terms of a
quantitative equivalence where we observe the termination in a certain
number of interaction steps.

**Viviana Bono: Types for (Slow) AI.**
Reasoning on knowledge bases is often done by machine learning models fed with
W3C Resource Description Framework data rather than by applying formal inference techniques.
On the one hand, this use of machine learning certainly provides a faster mechanism than any
formal (run time) inference technique, but, on the other hand, it may lead to an impoverishment
of the expressivity of the properties proven. Statically typed languages can help to attenuate
the performance issue: they offer the possibility of checking or inferring certain properties
of interest statically, meaning that they do not slow down run time. In this talk,
we will survey some already-present applications of types to knowledge representation
and give a hint about open problems.

Ugo de'Liguoro, Università di Torino, Italy

Riccardo Treglia, King’s College London, UK

- Mariangiola Dezani-Ciancaglini, Università di Torino, Italy
- Jakob Rehof, TU University of Dortmund, Germany
- Joe Wells, Heriot-Watt University, Scotland