Imperial College London

ProfessorNobukoYoshida

Faculty of EngineeringDepartment of Computing

Professor of Computing
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

307 results found

Yoshida N, Castro-Perez D, Ferreira Ruiz F, Gheri Let al., 2021, Zooid: A DSL for Certified Multiparty Computation:From Mechanised Metatheory to Certified Multiparty Processes, PLDI 2021, Publisher: Association for Computing Machinery (ACM)

Conference paper

Toninho B, Yoshida N, 2021, On polymorphic sessions and functions: A tale of two (fully abstract) encodings, ACM Transactions on Programming Languages and Systems, ISSN: 0164-0925

This work exploits the logical foundation of session types to determine what kind of type discipline for the𝜋-calculus can exactly capture, and is captured by, 𝜆-calculus behaviours. Leveraging the proof theoreticcontent of the soundness and completeness of sequent calculus and natural deduction presentations of linearlogic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processesencodings between a polymorphic session 𝜋-calculus and a linear formulation of System F. We are then ableto derive results of the session calculus from the theory of the 𝜆-calculus: (1) we obtain a characterisation ofinductive and coinductive session types via their algebraic representations in System F; and (2) we extend ourresults to account for value and process passing, entailing strong normalisation.

Journal article

Miu A, Ferreira Ruiz F, Yoshida N, Zhou Fet al., 2021, Communication-safe web programming in TypeScript with routed multiparty session types, The International Conference on Compiler Construction (CC), Publisher: ACM, Pages: 94-106

Modern web programming involves coordinating interactions between browser clients and a server. Typically, the interactions in web-based distributed systems are informally described, making it hard to ensure correctness, especially communication safety, i.e. all endpoints progress without type errors or deadlocks, conforming to a specified protocol.We present STScript, a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets, and RouST, a new session type theory that supports multiparty communications with routing mechanisms. STScript provides developers with TypeScript APIs generated from a communication protocol specification based on RouST. The generated APIs build upon TypeScript concurrency practices, complement the event-driven style of programming in full-stack web development, and are compatible with the Node.js runtime for server-side endpoints and the React.js framework for browser-side endpoints.RouST can express multiparty interactions routed via an intermediate participant. It supports peer-to-peer communication between browser-side endpoints by routing communication via the server in a way that avoids excessive serialisation. RouST guarantees communication safety for endpoint web applications written using STScript APIs.We evaluate the expressiveness of STScript for modern web programming using several production-ready case studies deployed as web applications.

Conference paper

Bravetti M, Carbone M, Lange J, Yoshida N, Zavattaro Get al., 2021, A sound algorithm for asynchronous session subtyping and its implementation, Logical Methods in Computer Science, ISSN: 1860-5974

Session types, types for structuring communication between endpoints in concurrent systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of systems, where a program has not precisely the expected behavior but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm. We use this tool to tes tour algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.

Journal article

Ghilezan S, Pantović J, Prokić I, Scalas A, Yoshida Net al., 2021, Precise subtyping for asynchronous multiparty sessions, POPL 2021, Publisher: Association for Computing Machinery (ACM), Pages: 1-28, ISSN: 2475-1421

Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T T′ holds, it is safe to replace an implementation of T′ with an implementation of the subtype T, which may allow for more optimised communication patterns.We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices).Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations — and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/outpu

Conference paper

Medic D, Mezzina CA, Phillips I, Yoshida Net al., 2020, A parametric framework for reversible pi-calculi, Information and Computation, Vol: 275, ISSN: 0890-5401

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality inπ-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework forreversibleπ-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversibleπ-calculus causal semantics.

Journal article

Zhou F, Ferreira F, Hu R, Neykova R, Yoshida Net al., 2020, Statically verified refinements for multiparty protocols, OOPSLA 2020, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421

With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom.While originally MPST focus on the communication aspects, and employ a simple typing system for communication payloads, communication protocols in the real world usually contain constraints on the payload. We introduce refined multiparty session types (RMPST), an extension of MPST, that express data dependent protocols via refinement types on the data types.We provide an implementation of RMPST, in a toolchain called Session*, using Scribble, a toolchain for multiparty protocols, and targeting F*, a verification-oriented functional programming language. Users can describe a protocol in Scribble and implement the endpoints in F* using refinement-typed APIs generated from the protocol. The F* compiler can then statically verify the refinements. Moreover, we use a novel approach of callback-styled API generation, providing static linearity guarantees with the inversion of control. We evaluate our approach with real world examples and show that it has little overhead compared to a naive implementation, while guaranteeing safety properties from the underlying theory.

Conference paper

Majumdar R, Yoshida N, Zufferey D, 2020, Multiparty motion coordination: from choreographies to robotics programs, OOPSLA 2020, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421

We present a programming model and typing discipline for complex multi-robot coordination programming. Our model encompasses both synchronisation through message passing and continuous-time dynamic motion primitives in physical space. We specify continuous-time motion primitives in an assume-guarantee logic that ensures compatibility of motion primitives as well as collision freedom. We specify global behaviour of programs in a choreographic type system that extends multiparty session types with jointly executed motion primitives, predicated refinements, as well as a separating conjunction that allows reasoning about subsets of interacting robots. We describe a notion of well-formedness for global types that ensures motion and communication can be correctly synchronised and provide algorithms for checking well-formedness, projecting a type, and local type checking. A well-typed program is communication safe, motion compatible, and collision free. Our type system provides a compositional approach to ensuring these properties. We have implemented our model on top of the ROS framework. This allows us to program multi-robot coordination scenarios on top of commercial and custom robotics hardware platforms. We show through case studies that we can model and statically verify quite complex manoeuvres involving multiple manipulators and mobile robots---such examples are beyond the scope of previous approaches.

Conference paper

Griesemer R, Hu R, Kokke W, Taylor IL, Toninho B, Wadler P, Yoshida Net al., 2020, Featherweight Go, OOPSLA 2020, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421

We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structural, and whereas generics in Java are defined via erasure, in Go we use monomorphisation. Although monomorphisation is widely used, we are one of the first to formalise it. Our design also supports a solution to The Expression Problem.

Conference paper

Castro-Perez D, Yoshida N, 2020, CAMP: cost-aware multiparty session protocols, OOPSLA 2020, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421

This paper presents CAMP, a new static performance analysis framework for message-passing concurrent and distributed systems, based on the theory of multiparty session types (MPST). Understanding the runtime performance of concurrent and distributed systems is of great importance for the identification ofbottlenecks and optimisation opportunities. In the message-passing setting, these bottlenecks are generallycommunication overheads and synchronisation times. Despite its importance, reasoning about these intensionalproperties of software, such as performance, has received little attention, compared to verifying extensionalproperties, such as correctness. Behavioural protocol specifications based on sessions types capture notonly extensional, but also intensional properties of concurrent and distributed systems. CAMP augmentsMPST with annotations of communication latency and local computation cost, defined as estimated executiontimes, that we use to extract cost equations from protocol descriptions. CAMP is also extendable to analyseasynchronous communication optimisation built on a recent advance of session type theories. We apply ourtool to different existing benchmarks and use cases in the literature with a wide range of communication protocols, implemented in C, MPI-C, Scala, Go, and OCaml. Our benchmarks show that, in most of the cases,we predict an upper-bound on the real execution costs with < 15% error.

Conference paper

Zhou F, Ferreira F, Hu R, Neykova R, Yoshida Net al., 2020, Statically verified refinements for multiparty protocols, Publisher: arXiv

With distributed computing becoming ubiquitous in the modern era, safedistributed programming is an open challenge. To address this, multipartysession types (MPST) provide a typing discipline for message-passingconcurrency, guaranteeing communication safety properties such as deadlockfreedom. While originally MPST focus on the communication aspects, and employ a simpletyping system for communication payloads, communication protocols in the realworld usually contain constraints on the payload. We introduce refinedmultiparty session types (RMPST), an extension of MPST, that express datadependent protocols via refinement types on the data types. We provide an implementation of RMPST, in a toolchain called Session*, usingScribble, a multiparty protocol description toolchain, and targeting F*, averification-oriented functional programming language. Users can describe aprotocol in Scribble and implement the endpoints in F* using refinement-typedAPIs generated from the protocol. The F* compiler can then statically verifythe refinements. Moreover, we use a novel approach of callback-styled APIgeneration, providing static linearity guarantees with the inversion ofcontrol. We evaluate our approach with real world examples and show that it haslittle overhead compared to a na\"ive implementation, while guaranteeing safetyproperties from the underlying theory.

Working paper

Medic D, Mezzina CA, Phillips I, Yoshida Net al., 2020, Towards a formal account for software transactional memory, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, ISSN: 0302-9743

Software transactional memory (STM) is a concurrency con-trol mechanism for shared memory systems. It is opposite to the lockbased mechanism, as it allows multiple processes to access the same setof variables in a concurrent way. Then according to the used policy, theeffect of accessing to shared variables can be committed (hence, madepermanent) or undone. In this paper, we define a formal framework fordescribing STMs and show how with a minor variation of the rules it ispossible to model two common policies for STM: reader preference andwriter preference.

Conference paper

Graversen E, Phillips I, Yoshida N, 2020, Event structures for the reversible early internal pi-calculus, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, ISSN: 0302-9743

The pi-calculus is a widely used process calculus, which models com-munications between processes and allows the passing of communication links.Various operational semantics of the pi-calculus have been proposed, which canbe classified according to whether transitions are unlabelled (so-called reductions)or labelled. With labelled transitions, we can distinguish early and late semantics.The early version allows a process to receive names it already knows from the en-vironment, while the late semantics and reduction semantics do not. All existingreversible versions of the pi-calculus use reduction or late semantics, despite theearly semantics of the (forward-only) pi-calculus being more widely used than thelate. We define piIH, the first reversible early pi-calculus, and give it a denotationalsemantics in terms of reversible bundle event structures. The new calculus is a re-versible form of the internal pi-calculus, which is a subset of the pi-calculus whereevery link sent by an output is private, yielding greater symmetry between inputsand outputs.

Conference paper

Yoshida N, Jongmans S-S, 2020, Exploring type-level bisimilarity towards more expressive multiparty session types, 29th European Symposium on Programming, Publisher: Springer, Pages: 251-279

A key open problem with multiparty session types (MPST)concerns their expressiveness: current MPST have inflexible choice, noexistential quantification over participants, and limited parallel compo-sition. This precludes many real protocols to be represented by MPST.To overcome these bottlenecks of MPST, we explore a new techniqueusing weak bisimilarity between global types and endpoint types, whichguarantees deadlock-freedom and absence of protocol violations. Basedon a process algebraic framework, we present well-formed conditions forglobal types that guarantee weak bisimilarity between a global type andits endpoint types and prove their check is decidable. Our main practicalresult, obtained through benchmarks, is that our well-formedness condi-tions can be checked orders of magnitude faster than directly checkingweak bisimilarity using a state-of-the-art model checker.

Conference paper

Yoshida N, Imai K, Neykova R, Yuen Set al., 2020, Multiparty session programming with global protocol combinators, 34th European Conference on Object-Oriented Programming, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, ISSN: 1868-8969

Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensuresthe absence of communication errors and deadlocks for well-typed communicating processes. Thestate-of-the-art implementations of the MPST theory rely on (1)runtime linearity checksto ensurecorrect usage of communication channels and (2) external domain-specific languages for specifyingand verifying multiparty protocols.To overcome these limitations, we propose a library for programming withglobal combinators– a set of functions for writing and verifying multiparty protocols in OCaml. Local behavioursforallprocesses in a protocol are inferredat oncefrom a global combinator. We formalise globalcombinators and prove a sound realisability of global combinators – a well-typed global combinatorderives a set of local types, by which typed endpoint programs can ensure type and communicationsafety. Our approach enables fully-static verification and implementation of the whole protocol, fromthe protocol specification to the process implementations, to happen in the same language.We compare our implementation to untyped and continuation-passing style implementations,and demonstrate its expressiveness by implementing a plethora of protocols. We show our librarycan interoperate with existing libraries and services, implementing DNS (Domain Name Service)protocol and the OAuth (Open Authentication) protocol.

Conference paper

Gabet J, Yoshida N, 2020, Static race detection and mutex safety and liveness for Go programs, 34th European Conference on Object-Oriented Programming (ECOOP) 2020, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, ISSN: 1868-8969

Go is a popular concurrent programming language thanks to its ability to efficiently combineconcurrency and systems programming. In Go programs, a number of concurrency bugs can becaused by a mixture of data races and communication problems. In this paper, we develop atheory based on behavioural types to statically detect data races and deadlocks in Go programs.We first specify lock safety/liveness and data race properties over a Go program model, using thehappens-before relation defined in the Go memory model. We represent these properties of programsin aμ-calculus model of types, and validate them using type-level model-checking. We then extendthe framework to account for Go’s channels, and implement a static verification tool which can detectconcurrency errors. This is, to the best of our knowledge, the first static verification framework ofthis kind for the Go language, uniformly analysing concurrency errors caused by a mix of sharedmemory accesses and asynchronous message-passing communications.

Conference paper

Miu A, Ferreira F, Yoshida N, Zhou Fet al., 2020, Generating Interactive WebSocket Applications in TypeScript, Electronic Proceedings in Theoretical Computer Science, Vol: 314, Pages: 12-22

Journal article

Castro-Perez D, Yoshida N, 2020, Compiling first-order functions to session-typed parallel code, ACM SIGPLAN 2020 International Conference on Compiler Construction (CC 2020), Publisher: ACM, Pages: 143-154

Building correct and efficient message-passing parallel pro-grams still poses many challenges. The incorrect use ofmessage-passing constructs can introduce deadlocks, anda bad task decomposition will not achieve good speedups.Current approaches focus either on correctness or efficiency,but limited work has been done on ensuring both. In thispaper, we propose a new parallel programming framework,PAlg, which is a first-order language withparticipant anno-tationsthat ensuresdeadlock-freedom by construction.PAlgprograms are coupled with an abstraction of their communi-cation structure, aglobal typefrom the theory ofmultipartysession types(MPST). This global type serves as an outputfor the programmer to assess the efficiency of their achievedparallelisation.PAlgis implemented as an EDSL in Haskell,from which we can: 1. compile to low-level message-passingC code; 2. compile to sequential C code, or interpret as se-quential Haskell functions; and, 3. infer the communicationprotocol followed by the compiled message-passing program.We use the properties of the inferred global types to performbasic message reordering optimisations to the compiled Ccode. We prove theextensional equivalenceof our outputparallelisation, as well as theprotocol compliance. We eval-uate our approach on a number of benchmarks. We achievelinear speedups on a shared-memory 12-core machine, anda speedup of 16 on a 2-node, 24-core NUMA.

Conference paper

Lagaillardie N, Neykova R, Yoshida N, 2020, Implementing multiparty session types in rust, Pages: 127-136, ISBN: 9783030500283

Multiparty Session Types (MPST) is a typing discipline for distributed protocols, which ensures communication safety and deadlock-freedom for more than two participants. This paper reports on our research project, implementing multiparty session types in Rust. Current Rust implementations of session types are limited to binary (two-party communications). We extend an existing library for binary session types to MPST. We have implemented a simplified Amazon Prime Video Streaming protocol using our library for both shared and distributed communication transports.

Book chapter

Ferreira Ruiz F, Yoshida N, Castro-Perez D, 2019, EMTST engineering the meta-theory of session types, International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Conference paper

Gheri L, Yoshida N, 2019, A Very Gentle Introduction to Multiparty Session Types, International Conference on Distributed Computing and Internet Technology

Conference paper

Yoshida N, Castro D, Ferreira F, 2019, EMTST - Engineering Meta-theory of Session Types

A Coq library to implement and reason about Session types. Together with a subject reduction for binary session types.

Software

Yoshida N, Medic D, 2019, RELATIVE EXPRESSIVENESS OF CALCULI FOR REVERSIBLE CONCURRENCY, BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE, Pages: 89-119, ISSN: 0252-9742

Journal article

Kouzapas D, Pérez JA, Yoshida N, 2019, On the relative expressiveness of higher-order session processes, Information and Computation, Vol: 268, Pages: 1-54, ISSN: 0890-5401

By integrating constructs from the λ-calculus and the π-calculus, in higher-order process calculiexchanged values may contain processes. This paper studies the relative expressiveness of HOπ,the higher-order π-calculus in which communications are governed by session types. Our maindiscovery is that HO, a subcalculus of HOπ which lacks name-passing and recursion, can serveas a new core calculus for session-typed higher-order concurrency. We show that HO can encodeHOπ fully abstractly (up to typed contextual equivalence) more precisely and efficiently than thefirst-order session π-calculus (π). Overall, under the discipline of session types, HOπ, HO, and πare equally expressive; however, we show that HOπ is more tightly related to HO than to π.

Journal article

Bravetti M, Carbone M, Lange J, Yoshida N, Zavattaro Get al., 2019, A sound algorithm for asynchronous session subtyping, 30th International Conference on Concurrency Theory, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 38:1-38:16, ISSN: 1868-8969

Session types, types for structuring communication between endpoints in distributed systems, arerecently being integrated into mainstream programming languages. In practice, a very importantnotion for dealing with such types is that of subtyping, since it allows for typing larger classes ofsystem, where a program has not precisely the expected behavior but a similar one. Unfortunately,recent work has shown that subtyping for session types in an asynchronous setting is undecidable.To cope with this negative result, the only approaches we are aware of either restrict the syntaxof session types or limit communication (by considering forms of bounded asynchrony). Bothapproaches are too restrictive in practice, hence we proceed differently by presenting an algorithm forchecking subtyping which is sound, but not complete (in some cases it terminates without returninga decisive verdict). The algorithm is based on a tree representation of the coinductive definition ofasynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence offinite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements ouralgorithm and we apply it to many examples that cannot be managed with the previous approaches.

Conference paper

Lange J, Yoshida N, 2019, Verifying asynchronous interactions via communicating session automata, 31st International Conference on Computer-Aided Verification (CAV), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 97-117, ISSN: 0302-9743

This paper proposes a sound procedure to verify properties of communicating session automata (csa), i.e., communicating automata that include multiparty session types. We introduce a new asynchronous compatibility property for csa, called k-multiparty compatibility (k-mc), which is a strict superset of the synchronous multiparty compatibility used in theories and tools based on session types. It is decomposed into two bounded properties: (i) a condition called k-safety which guarantees that, within the bound, all sent messages can be received and each automaton can make a move; and (ii) a condition called k-exhaustivity which guarantees that all k-reachable send actions can be fired within the bound. We show that k-exhaustivity implies existential boundedness, and soundly and completely characterises systems where each automaton behaves equivalently under bounds greater than or equal to k. We show that checking k-mc is pspace-complete, and demonstrate its scalability empirically over large systems (using partial order reduction).

Conference paper

Yoshida N, Neykova R, 2019, Featherweight Scribble, Models, Languages, and Tools for Concurrent and Distributed Programming, Editors: Boreale, Corradini, Loreti, Pugliese, Publisher: Springer, Pages: 236-259, ISBN: 978-3-030-21484-5

Thispapergivesaformaldefinitionoftheprotocolspeci-fication language Scribble. In collaboration with industry, Scribble hasbeen developed as an engineering incarnation of the formalmultipartysession types. In its ten years of development, Scribble has been appliedand extended in manyfold ways as to verify and ensure correctness ofconcurrent and distributed systems, e.g. type checking, runtime monitor-ing, code generation, and synthesis. This paper introduces a core versionof Scribble,Featherweight Scribble. We define the semantics of Scrib-ble by translation to communicating automata and show a behavioural-preserving encoding of Scribble protocols to multiparty session type.

Book chapter

Yoshida N, Majumdar R, Pirron M, Zufferey Det al., 2019, Motion session types for robotic interactions, European Conference on Object-Oriented Programming, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 28:1-28:27, ISSN: 1868-8969

Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning. We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via discrete messages as well as via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time. We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision. We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.

Conference paper

King J, Ng N, Yoshida N, 2019, Multiparty Session Type-safe Web Development with Static Linearity, 11th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric Software, Publisher: OPEN PUBL ASSOC, Pages: 35-46, ISSN: 2075-2180

Modern web applications can now offer desktop-like experiences from within the browser, thanksto technologies such as WebSockets, which enable low-latency duplex communication between thebrowser and the server. While these advances are great for the user experience, they represent anew responsibility for web developers who now need to manage and verify the correctness of morecomplex and potentially stateful interactions in their application.In this paper, we present a technique for developing interactive web applications that are stati-cally guaranteed to communicate following a given protocol. First, the global interaction protocol isdescribed in the Scribble protocol language – based on multiparty session types. Scribble protocolsare checked for well-formedness, and then each role is projected to a Finite State Machine represent-ing the structure of communication from the perspective of the role. We use source code generationand a novel type-level encoding of FSMs using multi-parameter type classes to leverage the typesystem of the target language and guarantee only programs that communicate following the protocolwill type check.Our work targets PureScript – a functional language that compiles to JavaScript – which cru-cially has an expressive enough type system to providestaticlinearity guarantees. We demonstratethe effectiveness of our approach through a web-based Battleship game where communication isperformed through WebSocket connections.

Conference paper

Altayeva A, Yoshida N, 2019, Service equivalence via multiparty session type isomorphisms, Publisher: arXiv

This paper addresses a problem found within the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We utilise the theory of Multiparty Session Types (MPST). Our approach is based upon the notion of a multiparty session type isomorphism, utilising a novel constructive realisation of service adapter code to establishing equivalence. We achieve this by employing trace semantics over a collection of local types and introducing meta abstractions over the syntax of global types. We develop a corresponding equational theory for MPST isomorphisms. The main motivation for this line of work is to define a type isomorphism that affords the assessment of whether two components/services are substitutables, modulo adaptation code given software components formalised as session types.

Working paper

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00365177&limit=30&person=true