ALC Seminar | Speaker: Silvia Ghilezan (Mathematical institute SASA & University of Novi Sad, Serbia)

Title: Duality of intersection and union types

Abstract: Intersection types are well-known for their ability to completely characterise strong normalisation in lambda calculus. As an implicit typing discipline, intersection types describe program behaviour without manifesting itself within the syntax of a program. Dually, union types offer a complementary implicit typing that extends the completeness property of intersection types. However, union types can easily break desirable meta-theoretical properties of the type system, such as subject reduction.

In this talk, based on joint work with Zena Ariola and Paul Downen, we discuss the design of type systems for both intersection and union types based on the duality of computation of the symmetric language of the classical sequent calculus.