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

181 results found

Bocchi L, Chen T-C, Demangeon R, Honda K, Yoshida Net al., 2017, Monitoring networks through multiparty session types, THEORETICAL COMPUTER SCIENCE, Vol: 669, Pages: 33-58, ISSN: 0304-3975

JOURNAL ARTICLE

Carbone M, Montesi F, Schurmann C, Yoshida Net al., 2017, Multiparty session types as coherence proofs, ACTA INFORMATICA, Vol: 54, Pages: 243-269, ISSN: 0001-5903

JOURNAL ARTICLE

Graversen E, Phillips I, Yoshida N, 2017, Towards a Categorical Representation of Reversible Event Structures, Publisher: OPEN PUBL ASSOC, Pages: 49-60, ISSN: 2075-2180

CONFERENCE PAPER

Hu R, Yoshida N, 2017, Explicit connection actions in multiparty session types, Pages: 116-133, ISSN: 0302-9743

© Springer-Verlag GmbH Germany 2017. This work extends asynchronous multiparty session types (MPST) with explicit connection actions to support protocols with optional and dynamic participants. The actions by which endpoints are connected and disconnected are a key element of real-world protocols that is not treated in existing MPST works. In addition, the use cases motivating explicit connections often require a more relaxed form of multiparty choice: these extensions do not satisfy the conservative restrictions used to ensure safety in standard syntactic MPST. Instead, we develop a modelling-based approach to validate MPST safety and progress for these enriched protocols. We present a toolchain implementation, for distributed programming based on our extended MPST in Java, and a core formalism, demonstrating the soundness of our approach. We discuss key implementation issues related to the proposed extensions: a practical treatment of choice subtyping for MPST progress, and multiparty correlation of dynamic binary connections.

CONFERENCE PAPER

Imai K, Yoshida N, Yuen S, 2017, Session-ocaml: A session-based library with polarities and lenses, Pages: 99-118, ISSN: 0302-9743

© IFIP International Federation for Information Processing 2017. We propose session-ocaml, a novel library for session-typed concurrent/distributed programming in OCaml. Our technique solely relies on parametric polymorphism, which can encode core session type structures with strong static guarantees. Our key ideas are: (1) polarised session types, which give an alternative formulation of duality enabling OCaml to automatically infer an appropriate session type in a session with a reasonable notational overhead; and (2) a parameterised monad with a data structure called ‘slots’ manipulated with lenses, which can statically enforce session linearity and delegations. We show applications of session-ocaml including a travel agency usecase and an SMTP protocol.

CONFERENCE PAPER

Kouzapas D, Perez JA, Yoshida N, 2017, Characteristic bisimulation for higher-order session processes, ACTA INFORMATICA, Vol: 54, Pages: 271-341, ISSN: 0001-5903

JOURNAL ARTICLE

Lange J, Ng N, Toninho B, Yoshida Net al., 2017, Fencing off Go: Liveness and Safety for Channel-Based Programming, 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Publisher: ASSOC COMPUTING MACHINERY, Pages: 748-761, ISSN: 0362-1340

CONFERENCE PAPER

Lange J, Yoshida N, 2017, On the undecidability of asynchronous session subtyping, Pages: 441-457, ISSN: 0302-9743

© Springer-Verlag GmbH Germany 2017. Asynchronous session subtyping has been studied extensively in [9, 10, 28–31] and applied in [23, 32, 33, 35] . An open question was whether this subtyping relation is decidable. This paper settles the question in the negative. To prove this result, we first introduce a new sub-class of two-party communicating finite-state machines (CFSMs), called asynchronous duplex (ADs), which we show to be Turing complete. Secondly, we give a compatibility relation over CFSMs, which is sound and complete wrt. safety for ADs, and is equivalent to the asynchronous subtyping. Then we show that the halting problem reduces to checking whether two CFSMs are in the relation. In addition, we show the compatibility relation to be decidable for three sub-classes of ADs.

CONFERENCE PAPER

Neykova R, Bocchi L, Yoshida N, 2017, Timed runtime monitoring for multiparty conversations, FORMAL ASPECTS OF COMPUTING, Vol: 29, Pages: 877-910, ISSN: 0934-5043

JOURNAL ARTICLE

Neykova R, Yoshida N, 2017, Let it recover: Multiparty protocol-induced recovery, Pages: 98-108

© 2017 ACM. Fault-tolerant communication systems rely on recovery strategies which are often error-prone (e.g. a programmer manually specifies recovery strategies) or inefficient (e.g. the whole system is restarted from the beginning). This paper proposes a static analysis based on multiparty session types that can efficiently compute a safe global state from which a system of interacting processes should be recovered. We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. We formalise our recovery algorithm and prove its safety. A recovered communication system is free from deadlocks, orphan messages and reception errors. Our recovery algorithm incurs less communication cost (only affected processes are notified) and overall execution time (only required states are repeated). On top of our analysis, we design and implement a runtime framework in Erlang where failed processes and their dependencies are soundly restarted from a computed safe state. We evaluate our recovery framework on messagepassing benchmarks and a use case for crawling webpages. The experimental results indicate our framework outperforms a built-in static recovery strategy in Erlang when a part of the protocol can be safely recovered.

CONFERENCE PAPER

Orchard D, Yoshida N, 2017, Special Issue: PLACES 2016 foreword, JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, Vol: 90, Pages: 1-1, ISSN: 2352-2208

JOURNAL ARTICLE

Scalas A, Yoshida N, 2017, Multiparty Session Types, Beyond Duality (Abstract), Publisher: OPEN PUBL ASSOC, Pages: 37-38, ISSN: 2075-2180

CONFERENCE PAPER

Toninho B, Yoshida N, 2017, Certifying data in multiparty session types, JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, Vol: 90, Pages: 61-83, ISSN: 2352-2208

JOURNAL ARTICLE

Ancona D, Bono V, Bravetti M, Campos J, Castagna G, Denielou P-M, Gay SJ, Gesbert N, Giachino E, Hu R, Johnsen EB, Martins F, Mascardi V, Montesi F, Neykova R, Ng N, Padovani L, Vasconcelos VT, Yoshida Net al., 2016, Behavioral Types in Programming Languages, FOUNDATIONS AND TRENDS IN PROGRAMMING LANGUAGES, Vol: 3, Pages: I-+, ISSN: 2325-1107

JOURNAL ARTICLE

Debois S, Hildebrandt T, Slaats T, Yoshida Net al., 2016, TYPE-CHECKING LIVENESS FOR COLLABORATIVE PROCESSES WITH BOUNDED AND UNBOUNDED RECURSION, LOGICAL METHODS IN COMPUTER SCIENCE, Vol: 12, ISSN: 1860-5974

JOURNAL ARTICLE

Debois S, Hildebrandt T, Slaats T, Yoshida Net al., 2016, Type-checking liveness for collaborative processes with bounded and unbounded recursion, Logical Methods in Computer Science, Vol: 12

© S. Debois, T. Hildebrandt, T. Slaats, and N. Yoshida. We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (databased) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.

JOURNAL ARTICLE

Dezani-Ciancaglini M, Ghilezan S, Jakšić S, Pantović J, Yoshida Net al., 2016, Denotational and operational preciseness of subtyping: A roadmap, Pages: 155-172, ISBN: 9783319307336

© Springer International Publishing Switzerland 2016. The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in object-oriented programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type, which is a mathematical object describing the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The present paper shows that standard proofs of operational preciseness imply denotational preciseness and gives an overview on this subject.

BOOK CHAPTER

Dezani-Ciancaglini M, Ghilezan S, Jaksic S, Pantovic J, Yoshida Net al., 2016, Precise subtyping for synchronous multiparty sessions, ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, Pages: 29-43, ISSN: 2075-2180

JOURNAL ARTICLE

Honda K, Yoshida N, Carbone M, 2016, Multiparty Asynchronous Session Types, JOURNAL OF THE ACM, Vol: 63, ISSN: 0004-5411

JOURNAL ARTICLE

Hu R, Yoshida N, 2016, Hybrid Session Verification Through Endpoint API Generation, 19th International Conference on Fundamental Approaches to Software Engineering (FASE) held as part of Annual European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 401-418, ISSN: 0302-9743

CONFERENCE PAPER

Kouzapas D, Perez JA, Yoshida N, 2016, On the Relative Expressiveness of Higher-Order Session Processes, 25th European Symposium on Programming (ESOP) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 446-475, ISSN: 0302-9743

CONFERENCE PAPER

Lange J, Yoshida N, 2016, Characteristic Formulae for Session Types, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 833-850, ISSN: 0302-9743

CONFERENCE PAPER

Mycroft A, Orchard DA, Petricek T, 2016, Effect Systems Revisited - Control-Flow Algebra and Semantics., Semantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, Editors: Probst, Hankin, Hansen, Publisher: Springer, Pages: 1-32, ISBN: 978-3-319-27809-4

BOOK CHAPTER

Ng N, Yoshida N, 2016, Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis, 25th International Conference on Compiler Construction (CC), Publisher: ASSOC COMPUTING MACHINERY, Pages: 174-184

CONFERENCE PAPER

Niu X, Ng N, Yuki T, Wang S, Yoshida N, Luk Wet al., 2016, EURECA Compilation: Automatic Optimisation of Cycle-Reconfigurable Circuits, 26th International Conference on Field-Programmable Logic and Applications (FPL), Publisher: IEEE, ISSN: 1946-1488

CONFERENCE PAPER

Orchard D, Yoshida N, 2016, Effects as Sessions, Sessions as Effects, 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Publisher: ASSOC COMPUTING MACHINERY, Pages: 568-581, ISSN: 0362-1340

CONFERENCE PAPER

Orchard D, Yoshida N, 2016, Using session types as an effect system, ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, Pages: 1-13, ISSN: 2075-2180

JOURNAL ARTICLE

Orchard D, Yoshida N, 2016, Electronic Proceedings in Theoretical Computer Science, EPTCS: Preface, ISSN: 2075-2180

CONFERENCE PAPER

Perera R, Lange J, Gay S, 2016, Multiparty compatibility for concurrent objects, International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, Publisher: Open Publishing Association, Pages: 73-82, ISSN: 2075-2180

Objects and actors are communicating state machines, offering and consuming different services atdifferent points in their lifecycle. Two complementary challenges arise when programming suchsystems. When objects interact, their state machines must be “compatible”, so that services arerequested only when they are available. Dually, when objects refine other objects, their state machinesmust be “compliant”, so that services are honoured whenever they are promised.In this paper we show how the idea of multiparty compatibility from the session types literaturecan be applied to both of these problems. We present an untyped language in which concurrent objectsare checked automatically for compatibility and compliance. For simple objects, checking can beexhaustive and has the feel of a type system. More complex objects can be partially validated via testcases, leading to a methodology closer to continuous testing. Our proof-of-concept implementationis limited in some important respects, but demonstrates the potential value of the approach and therelationship to existing software development practices.

CONFERENCE PAPER

Scalas A, Yoshida N, 2016, Lightweight session programming in scala, Pages: 211-2128, ISSN: 1868-8969

© Alceste Scalas and Nobuko Yoshida; licensed under Creative Commons License CC-BY. Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style Protocols (CPSPs), studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.

CONFERENCE 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