Capable : a mechanised imperative language with native multiparty session types

Muijnck-Hughes, Jan de and Urlea, Cristian and Voinea, Laura and Vanderbauwhede, Wim (2023) Capable : a mechanised imperative language with native multiparty session types. In: ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, 2023-10-22 - 2023-10-27.

[thumbnail of de-Muijnck-Hughes-etal-SPLASH-2023-Capable-a-mechanised-imperative-language-with-native-multiparty-session-types]
Preview
 Text. Filename: de-Muijnck-Hughes-etal-SPLASH-2023-Capable-a-mechanised-imperative-language-with-native-multiparty-session-types.pdf
Accepted Author Manuscript
License: Creative Commons Attribution 4.0 logo
Download (672kB)| Preview

Abstract

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.

CORE (COnnecting REpositories)