Capable: a mechanised imperative language with native multiparty session types

Jan de Muijnck-Hughes; Cristian Urlea; Laura Voinea; Wim Vanderbauwhede

Capable: a mechanised imperative language with native multiparty session types

Jan de Muijnck-Hughes, Cristian Urlea, Laura Voinea, Wim Vanderbauwhede

Research output: Contribution to conference › Paper › peer-review

51 Downloads (Pure)

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.

Original language	English
Number of pages	7
Publication status	Published - 27 Oct 2023
Event	ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity - Lisbon, Portugal Duration: 22 Oct 2023 → 27 Oct 2023 https://2023.splashcon.org/

Conference

Conference	ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity
Abbreviated title	SPLASH 2023
Country/Territory	Portugal
City	Lisbon
Period	22/10/23 → 27/10/23
Internet address	https://2023.splashcon.org/

Keywords

mechanised imperative language
Multiparty Session Types
mechanisation

Access to Document

de-Muijnck-Hughes-etal-SPLASH-2023-Capable-a-mechanised-imperative-language-with-native-multiparty-session-typesAccepted author manuscript, 657 KBLicence: CC BY 4.0

Cite this

@conference{4d9170063cc04bcea655e3a11018e0c3,

title = "Capable: a mechanised imperative language with native multiparty session types",

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.",

keywords = "mechanised imperative language, Multiparty Session Types, mechanisation",

author = "Muijnck-Hughes, {Jan de} and Cristian Urlea and Laura Voinea and Wim Vanderbauwhede",

note = "Note: the presentation of this paper at the conference was cancelled.; ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH 2023 ; Conference date: 22-10-2023 Through 27-10-2023",

year = "2023",

month = oct,

day = "27",

language = "English",

url = "https://2023.splashcon.org/",

}

TY - CONF

T1 - Capable

T2 - ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity

AU - Muijnck-Hughes, Jan de

AU - Urlea, Cristian

AU - Voinea, Laura

AU - Vanderbauwhede, Wim

N1 - Note: the presentation of this paper at the conference was cancelled.

PY - 2023/10/27

Y1 - 2023/10/27

N2 - 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.

AB - 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.

KW - mechanised imperative language

KW - Multiparty Session Types

KW - mechanisation

UR - https://eprints.gla.ac.uk/305386/

M3 - Paper

Y2 - 22 October 2023 through 27 October 2023

ER -

Capable: a mechanised imperative language with native multiparty session types

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this