[TYPES/announce] ITRS 2020: FInal Call for Papers (Due on 10 Jan, 2020)

[Riccardo Treglia]

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

Program Committee

Ugo de' Liguoro (University of Turin)

Jeremy Siek  (Indiana University Bloomington)

Andrej Dudenhefner (Saarland University)

Antonio Bucciarelli (Université 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)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20200103/135dfb39/attachment-0001.html>