[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
∧ 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 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
Organizer
Ugo de' Liguoro (Università di Torino, Italy)
Steering Committee
Mariangiola Dezani-Ciancaglini (Università di Torino, Italy)
Jakob Rehof (University of Dortmund, Germany)
Joe Wells (Heriot-Watt University, Scotland)
--
Ugo de'Liguoro
Associate Professor of Computer Science
Dipartimento di Informatica
Università di Torino
Corso Svizzera 185, 10149, Torino, Italy
