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

200 results found

Franco J, Clebsch S, Drossopoulou S, Vitek J, Wrigstad Tet al., 2018, Correctness of a concurrent object collector for actor languages, Pages: 885-911, ISSN: 0302-9743

© The Author(s) 2018. ORCA is a garbage collection protocol for actor-based programs. Multiple actors may mutate the heap while the collector is running without any dedicated synchronisation. ORCA is applicable to any actor language whose type system prevents data races and which supports causal message delivery. We present a model of ORCA which is parametric to the host language and its type system. We describe the interplay between the host language and the collector. We give invariants preserved by ORCA, and prove its soundness and completeness.

CONFERENCE PAPER

Scalas A, Yoshida N, 2018, Multiparty session types, beyond duality, JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, Vol: 97, Pages: 55-84, ISSN: 2352-2208

JOURNAL ARTICLE

Toninho B, Yoshida N, 2018, Depending on session-typed processes, Pages: 128-145, ISSN: 0302-9743

© The Author(s) 2018. This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed λ -calculus. The proposed framework, by allowing session processes to depend on functions and vice-versa, enables us to specify and statically verify protocols where the choice of the next communication action can depend on specific values of received data. Moreover, the type theoretic nature of the framework endows us with the ability to internally describe and prove predicates on process behaviours. Our main results are type soundness of the framework, and a faithful embedding of the functional layer of the calculus within the session-typed layer, showcasing the expressiveness of dependent session types.

CONFERENCE PAPER

Toninho B, Yoshida N, 2018, On polymorphic sessions and functions: A tale of two (fully abstract) encodings, Pages: 827-855, ISSN: 0302-9743

© The Author(s) 2018. 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 theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π -calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ -calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

CONFERENCE PAPER

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

Chen T-C, Dezani-Ciancaglini M, Scalas A, Yoshida Net al., 2017, ON THE PRECISENESS OF SUBTYPING IN SESSION TYPES, LOGICAL METHODS IN COMPUTER SCIENCE, Vol: 13, ISSN: 1860-5974

JOURNAL ARTICLE

Clebsch S, Franco J, Drossopoulou S, Yang AM, Wrigstad T, Vitek Jet al., 2017, Orca: GC and type system co-design for actor languages, Pages: 1-28

CONFERENCE PAPER

Franco J, Hagelin M, Wrigstad T, Drossopoulou S, Eisenbach Set al., 2017, You can have it all: Abstraction and good cache performance, Pages: 148-167

© 2017 Copyright held by the owner/author(s). On current architectures, the optimisation of an application's performance often involves data being stored according to access affinity - what is accessed together should be stored together, rather than logical affinity - what belongs together logically stays together. Such low level techniques lead to faster, but more error prone code, and end up tangling the program's logic with low-level data layout details. Our vision, which we call SHAPES - Safe, High-level, Abstractions for oPtimisation of mEmory cacheS - is that the layout of a data structure should be defined only once, upon instantiation, and the remainder of the code should be layout agnostic. This enables performance improvements while also guaranteeing memory safety, and supports the separation of program logic from low level concerns. In this paper we investigate how this vision can be supported by extending a programming language. We describe the core language features supporting this vision: classes can be customized to support different layouts, and layout information is carried around in types; the remaining source code is layout-unaware and the compiler emits layout-aware code. We then discuss our SHAPES implementation through a prototype library, which we also used for preliminary evaluations. Finally, we discuss how the core could be expanded so as to deliver SHAPES's full potential: the incorporation of compacting garbage collection, ad hoc polymorphism and late binding, synchronization of representations of different collections, support for dynamic change of representation, etc.

CONFERENCE PAPER

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, 20th International Conference on Fundamental Approaches to Software Engineering (FASE) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 116-133, ISSN: 0302-9743

CONFERENCE PAPER

Imai K, Yoshida N, Yuen S, 2017, Session-ocaml: A Session-Based Library with Polarities and Lenses, 19th IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION) Held as Part of the 12th International Federated Conference on Distributed Computing Techniques (DisCoTec), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 99-118, ISSN: 0302-9743

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, Tuosto E, Yoshida N, 2017, A Tool for Choreography-Based Analysis of Message-Passing Software, Behavioural Types: from Theory to Tools

BOOK CHAPTER

Lange J, Yoshida N, 2017, On the Undecidability of Asynchronous Session Subtyping, 20th International Conference on Foundations of Software Science and Computation Structures (FOSSACS) held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 441-457, ISSN: 0302-9743

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

Neykova R, Yoshida N, 2017, MULTIPARTY SESSION ACTORS, LOGICAL METHODS IN COMPUTER SCIENCE, Vol: 13, ISSN: 1860-5974

JOURNAL ARTICLE

Ng CWN, Yoshida N, 2017, Protocol-Driven MPI Program Generation, Behavioural Types: from Theory to Tools

BOOK CHAPTER

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

Orchard D, Yoshida N, 2017, Session Types with Linearity in Haskell, Behavioural Types: from Theory to Tools

BOOK CHAPTER

Scalas A, Dardha O, Hu R, Yoshida Net al., 2017, A linear decomposition of multiparty sessions for safe distributed programming, Pages: 241-2431, ISSN: 1868-8969

Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages? We address this problem by (1) developing the first encoding of a full-fledged multiparty session π-calculus into linear π-calculus, and(2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala. Our encoding is type-preserving and operationally sound and complete. Crucially, it keeps the distributed choreographic nature of MPST, illuminating that the safety properties of multiparty sessions can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty and binary sessions via centralised orchestration means. We exploit these results to implement an automated generation of Scala APIs for multiparty sessions, abstracting existing libraries for binary communication channels. This allows multiparty systems to be safely implemented over binary message transports, as commonly found in practice. Our implementation is the first to support distributed multiparty delegation: Our encoding yields it for free, via existing mechanisms for binary delegation.

CONFERENCE PAPER

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

Vasconcelos VT, Martins F, Marques ERB, Yoshida N, Ng CWNet al., 2017, Deductive Verification of MPI Protocols, Behavioural Types: from Theory to Tools

BOOK CHAPTER

Yoshida N, Neykova R, 2017, How to Verify Your Python Conversations, Behavioural Types: from Theory to Tools, Editors: Gay, Ravara

BOOK CHAPTER

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

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