30 Years of Session TypesST30

Session types are a type-theoretic approach to specifying communication protocols so that they can be verified by type-checking. This year marks 30 years since the first paper on session types, by Kohei Honda at CONCUR 1993. Since then the topic has attracted increasing interest, and a substantial community and literature have developed. Google Scholar lists almost 400 articles with “session types” in the title, and most programming language conferences now include several papers on session types each year. In terms of the technical focus, there have been continuing theoretical developments (notably the generalisation from two-party to multi-party session types by Honda, Yoshida and Carbone in 2008, and the development of a Curry-Howard correspondence with linear logic by Caires and Pfenning in 2010) and a variety of implementations of session types as programming language extensions or libraries, covering (among others) Haskell, OCaml, Java, Scala, Rust, Python, C#, Go.

This workshop will celebrate the 30th anniversary of session types by bringing together the community for a day of talks and technical discussion. The programme will include invited talks, contributed talks, and a panel session on future directions for session types.

Call for Papers

Session types are a type-theoretic approach to specifying communication protocols so that they can be verified by type-checking. This year marks 30 years since the first paper on session types, by Kohei Honda at CONCUR 1993. Since then the topic has attracted increasing interest, and a substantial community and literature have developed. Theoretical landmarks, each spawning substantial subfields, include the generalisation from two-party to multi-party session types by Honda, Yoshida and Carbone in 2008, and the development of a Curry-Howard correspondence with linear logic by Caires and Pfenning in 2010. Connections have been established with model-checking, dependent type theory, denotational semantics, mechanised metatheory, semantic typing and other topics. Implementations of session types as programming language extensions or libraries cover (among others) Haskell, OCaml, Java, Scala, Rust, Python, C#, Go.

We invite submissions to a workshop celebrating 30 years of session types. Submissions can be about any aspect of session types, including but not limited to the topics listed above. The programme will include invited talks, contributed talks and a panel session.

We call for three types of submission:

• Research papers with a maximum length of 8 pages (excluding bibliography and appendices). Submitted research papers will be reviewed for novelty, clarity and technical soundness. They must not be submitted simultaneously for publication in other venues. Accepted research papers will appear in the workshop proceedings.

• Talk proposals with a maximum length of 2 pages (excluding bibliography and appendices). Talk proposals can be for presentation of ongoing work, or for presentation of work that has already been published elsewhere. Proposals will be reviewed based on their likely interest as contributions to the workshop. Accepted talks will be presented at the workshop, but will not have corresponding papers in the workshop proceedings.

• Demo proposals with a maximum length of 2 pages (excluding bibliography and appendices). Demo proposals can be for any programming language, library, tool or other software that is based on session types. Accepted demos will be presented at the workshop, but will not have corresponding papers in the workshop proceedings.

Submissions must be formatted in EPTCS style. We intend the proceedings to be published in EPTCS.