SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Sun 22 Oct 2023 14:00 - 14:30 at Room XIII - ST30 Day 1 Session 3 Chair(s): Peter Thiemann

CAPABLE is lightweight mechanised imperative language that provides native support for Multiparty Session Types (MPSTs). Through mechanisation, we can explore and catalogue the changes required to extend similar languages with native support for MPSTs, as well as the interplay between the existing type-system and other novel extensions. Principally, our demo shows CAPABLE in action and what a language with native MPSTs can look like. We also look beneath the surface syntax and offer insight over how we created intrinsically typed sessions (and session types) within a dependently typed language. We show a compact well-scoped encoding of session types, mechanised proofs of soundness and completeness for projection, and how dependent types help with bidirectional type checking of typed sessions.

Sun 22 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
ST30 Day 1 Session 3ST30 at Room XIII
Chair(s): Peter Thiemann University of Freiburg, Germany
14:00
30m
Talk
CAPABLE: A Mechanised Imperative Language with Native Multiparty Session TypesCancelled
ST30
Jan de Muijnck-Hughes University of Strathclyde, Cristian Urlea , Adriana Laura Voinea , Wim Vanderbauwhede University of Glasgow
14:30
30m
Talk
Complete Multiparty Session Type Projection with Automata
ST30
Elaine Li NYU, Felix Stutz MPI-SWS, Thomas Wies New York University, Damien Zufferey SonarSource
15:00
30m
Talk
Multiparty Reactive Sessions
ST30
Ilaria Castellani INRIA Sophia Antipolis, France, Cinzia Di Giusto Université Côte d'Azur; CNRS, Jorge A. Pérez University of Groningen
Link to publication File Attached