CAPABLE: A Mechanised Imperative Language with Native Multiparty Session TypesCancelled
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 OctDisplayed time zone: Lisbon change
14:00 - 15:30 | |||
14:00 30mTalk | 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 30mTalk | Complete Multiparty Session Type Projection with Automata ST30 | ||
15:00 30mTalk | 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 |