Wed 17 Jul 2019 14:10 - 14:30 at Mancy - Types Chair(s): Davide Ancona

Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the π-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols.

Here we study minimal session types, session types without sequencing. This is arguably the simplest form of session types. By relying on a core process calculus with sessions and higher-order concurrency (abstraction passing), we prove that every process typable with usual (non minimal) session types can be compiled down into a process typed with minimal session types. This means that having sequencing constructs in both processes and session types is redundant; only sequentiality in processes is indispensable, as it can precisely codify sequentiality in types.

Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow’s results in the realm of typed processes, our results reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into languages without sequencing in types.

Wed 17 Jul

Displayed time zone: Belfast change

13:30 - 15:10
TypesResearch Papers at Mancy
Chair(s): Davide Ancona University of Genova
13:30
20m
Research paper
Transient Typechecks are (Almost) Free
Research Papers
Richard Roberts Victoria University of Wellington, Stefan Marr University of Kent, Michael Homer Victoria University of Wellington, James Noble Victoria University of Wellington
DOI Media Attached
13:50
20m
Research paper
A Typing Discipline for Hardware Interfaces
Research Papers
Jan de Muijnck-Hughes University of Glasgow, Wim Vanderbauwhede University of Glasgow
DOI Media Attached
14:10
20m
Research paper
Minimal Session TypesPearl
Research Papers
Alen Arslanagić University of Groningen, Jorge A. Pérez University of Groningen, The Netherlands, Erik Voogd University of Oslo
DOI Media Attached
14:30
20m
Research paper
Julia's Efficient Algorithm for Subtyping Unions and Covariant TuplesPearl
Research Papers
Benjamin Chung Northeastern University, Francesco Zappa Nardelli Inria, Jan Vitek Northeastern University
DOI Media Attached
14:50
20m
Research paper
On Satisfiability of Nominal Subtyping with Variance
Research Papers
Aleksandr Misonizhnik Saint-Petersburg State University, Dmitry Mordvinov Saint-Petersburg State University, JetBrains Research
DOI Media Attached