Session Types for Reliable Distributed Systems (STARDUST)
Lead Research Organisation:
Imperial College London
Department Name: Computing
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
People |
ORCID iD |
Nobuko Yoshida (Principal Investigator) |
Publications
Barwell A
(2022)
Book review
in Journal of Logical and Algebraic Methods in Programming
Barwell Ad
(2022)
Generalised Multiparty Session Types with Crash-Stop Failures
Bravetti M
(2021)
A Sound Algorithm for Asynchronous Session Subtyping and its Implementation.
in Logical Methods in Computer Science
Bravetti Mario
(2021)
A SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING AND ITS IMPLEMENTATION
in LOGICAL METHODS IN COMPUTER SCIENCE
Castro-Perez D
(2021)
Zooid: a DSL for Certified Multiparty Computation
Castro-Perez D
(2020)
CAMP: cost-aware multiparty session protocols
in Proceedings of the ACM on Programming Languages
Castro-Perez D
(2020)
CAMP: Cost-Aware Multiparty Session Protocols
Description | Implementing multiparty session types with Rust for two versions, synchronous version and asynchronous version. |
Exploitation Route | Yes for the education and other UKRI projects such as AppControl and Morello-HAT. |
Sectors | Digital/Communication/Information Technologies (including Software) Education Financial Services and Management Consultancy |
URL | https://mrg.cs.ox.ac.uk/ |
Description | It is used for Morello-HAT and AppControl Projects which are related to Morello boards. The tools are also used for educations at Imperial and Keio University in Japan. |
First Year Of Impact | 2022 |
Sector | Digital/Communication/Information Technologies (including Software),Education,Security and Diplomacy |
Impact Types | Economic |
Title | Artifact: Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types |
Description | Artifact of the paper: "Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types", PPoPP 2022. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | The Rumpsteak framework is a framework for MPST in Rust. This software is an artifact that shows its capabilities. |
URL | https://zenodo.org/record/5786034 |
Title | Artifact: Design-By-Contract for Flexible Multiparty Session Protocols |
Description | Artifact for the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.21 |
Title | Artifact: Dynamically Updatable Multiparty Session Protocols |
Description | Artifact for the paper: Dynamically Updatable Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Dynamically Updatable Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.10 |
Title | Artifact: Generalised Multiparty Session Types with Crash-Stop Failures |
Description | Artifact supporting the paper : Generalised Multiparty Session Types with Crash-Stop Failures |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for the paper : https://github.com/alcestes/mpstk-crash-stop |
URL | https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.35 |
Title | Artifact: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Description | Artifact for paper: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for paper : Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
URL | https://dl.acm.org/doi/10.1145/3563331 |
Title | Artifact: Rollback Recovery in Session-Based Programming |
Description | Artifact for paper: Rollback Recovery in Session-Based Programming |
Type Of Technology | Software |
Year Produced | 2023 |
Impact | Artifact for paper: Rollback Recovery in Session-Based Programming |
URL | https://link.springer.com/chapter/10.1007/978-3-031-35361-1_11#chapter-info |
Title | Artifact: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types |
Description | Artifact for the paper: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (https://doi.org/10.4230/DARTS.8.2.9) This introduces the `multicrusty` library. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper. |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.9 |
Title | Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact) |
Description | We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop fail- ures and crash-handling behaviours. Teatrino accompanies the novel MPST theory in the related article, and enables users to generate fault-tolerant protocol-conforming Scala code from Scribble protocols. Local types are projected from the global protocol, enabling correctness-by-construction, and are expressed directly as Scala types via the Effpi concurrency library. Teatrino extends both Scribble and Effpi with support for crash-stop behaviour. The generated Scala code is execut- able and can be further integrated with existing systems. The accompanying theory in the related article guarantees deadlock-freedom and liveness properties for failure handling protocols and their implementation. This artifact includes examples, extended from both session type and distributed systems literature, featured in the related article. |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Designing Asynchronous Multiparty Protocols with Crash-Stop Failures |
URL | https://zenodo.org/record/7974824 |
Title | Zooid: a DSL for Certified Multiparty Computation |
Description | Artifact for the Zooid language and Coq mechanisation of the metathory of multiparty session types. This artifact contains the implementation for "Zooid: a DSL for Certified Multiparty Computation" from PLDI'21 This code is maintained at: https://github.com/emtst/zooid-cmpst |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | See: http://mrg.doc.ic.ac.uk/publications/zooid-paper/ |
URL | https://zenodo.org/record/4581294 |
Title | dot-parser |
Description | A parser for DOT files in Rust |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | No such parser previously existed in Rust. This is used for the developement of the Rumpsteak framework. |
URL | https://crates.io/crates/dot-parser |