Nobuko Yoshida

TCS Journal 2026 Journal Article

Less is more revisited: Association with global protocols and multiparty sessions

• Ping Hou
• Nobuko Yoshida
• Iona Kuhn

Ensuring correctness of communication in distributed systems remains challenging. To address this, Multiparty session types (MPST), initially introduced by Honda et al. [1, 2], offer a type discipline in which a programmer or architect specifies an overall view of communication as a global protocol (global type), and each distributed program is locally type-checked against its end-point projection. In practice, the MPST framework has been integrated into over 25 programming languages or tools. Ten years after the emergence of MPST, Scalas and Yoshida [3] discovered that existing proofs of type safety using end-point projection with mergeability are flawed, where the mergeability operator enlarges the typability of MPST end-point programs, admits easy implementation, and is more efficient than alternative approaches, including model checking. Nevertheless, following the result in Scalas and Yoshida [3], the soundness of end-point projection (with mergeability) has been interpreted in the literature as problematic. We clarify this concern by proposing a new general proof technique for type soundness (subject reduction) of multiparty session π-calculus, which relies on an association relation between the behavioural semantics of a global type and its end-point projection. With this approach, behavioural properties, namely session fidelity, deadlock freedom, and liveness, are also guaranteed based on global types. Additionally, we provide detailed comparisons with existing MPST typing systems and discuss their respective proof methods for type soundness.

I&C Journal 2024 Journal Article

Mixed choice in session types

• Kirstin Peters
• Nobuko Yoshida

Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the π-calculus where mixed choice was proved more expressive. Recently Casal, Mordido, and Vasconcelos proposed binary session types with mixed choices ( CMV + ). Surprisingly, in spite of an inclusion of unrestricted channels with mixed choice, CMV + 's mixed choice is rather separate and not mixed. We prove this negative result using two methodologies (using either the leader election problem or a synchronisation pattern as distinguishing feature), showing that there exists no good encoding from the π-calculus into CMV +, preserving distribution. We then close their open problem on the encoding from CMV + into CMV (without mixed choice), proving its soundness.

I&C Journal 2023 Journal Article

Causal computational complexity of distributed processes

• Romain Demangeon
• Nobuko Yoshida

This article studies the complexity of π-calculus processes with respect to the quantity of transitions caused by an incoming message. First, we propose a typing system for integrating Bellantoni and Cook's characterisation of polytime computable functions into Deng and Sangiorgi's typing system for termination. We then define computational complexity of distributed messages based on Degano and Priami's causal semantics, which identifies the dependency between interleaved transitions. Next, we apply a necessary syntactic flow analysis to typable processes to ensure a computational bound on the number of distributed messages. We prove that our analysis is decidable; sound in the sense that it guarantees that the total number of messages causally dependent of an input request received from the outside is bounded by a polynomial of the content of this request; and complete, meaning that each polynomial recursive function can be computed by a typable process.

I&C Journal 2020 Journal Article

A parametric framework for reversible π-calculi

• Doriana Medić
• Claudio Antares Mezzina
• Iain Phillips
• Nobuko Yoshida

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 for reversible π-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.

I&C Journal 2019 Journal Article

On the relative expressiveness of higher-order session processes

• Dimitrios Kouzapas
• Jorge A. Pérez
• Nobuko Yoshida

By integrating constructs from the λ-calculus and the π-calculus, in higher-order process calculi exchanged 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 main discovery is that HO, a subcalculus of HO π which lacks name-passing and recursion, can serve as a new core calculus for session-typed higher-order concurrency. We show that HO can encode HO π fully abstractly (up to typed contextual equivalence) more precisely and efficiently than the first-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 π.

TCS Journal 2017 Journal Article

Monitoring networks through multiparty session types

• Laura Bocchi
• Tzu-Chun Chen
• Romain Demangeon
• Kohei Honda
• Nobuko Yoshida

In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored π-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i. e. equating networks offering the same services to a user. We illustrate our static–dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.

I&C Journal 2015 Journal Article

Session typing and asynchronous subtyping for the higher-order π-calculus

• Dimitris Mostrous
• Nobuko Yoshida

This paper proposes a session typing system for the higher-order π-calculus (the HOπ-calculus) with asynchronous communication subtyping, which allows partial commutativity of actions in higher-order processes. The system enables two complementary kinds of optimisation, mobile code and asynchronous permutation of session actions, within processes that utilise structured, typed communications. Our first contribution is a session typing system for the HOπ-calculus using techniques from the linear λ-calculus. Integration of arbitrary higher-order code mobility and sessions leads to technical difficulties in type soundness, because linear usage of session channels and completion of sessions are required. Our second contribution is to introduce an asynchronous subtyping system which uniformly deals with type-manifested asynchrony and linear functions. The most technical challenge for subtyping is to prove the transitivity of the subtyping relation. We also demonstrate the expressiveness of our typing system with an e-commerce example, where optimised processes can interact respecting the expected sessions.

TCS Journal 2014 Journal Article

An observationally complete program logic for imperative higher-order functions

• Kohei Honda
• Nobuko Yoshida
• Martin Berger

We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state.

TCS Journal 2010 Journal Article

Typed event structures and the linear π -calculus

• Daniele Varacca
• Nobuko Yoshida

We propose a typing system for the true concurrent model of event structures that guarantees the interesting behavioural properties known as conflict freeness and confusion freeness. Conflict freeness is the true concurrent version of the notion of confluence. A system is confusion free if nondeterministic choices are localised and do not depend on the scheduling of independent components. Ours is the first typing system to control behaviour in a true concurrent model. To demonstrate its applicability, we show that typed event structures give a semantics of linearly typed version of the π -calculi with internal mobility. The semantics we provide is the first event structure semantics of the π -calculus and generalises Winskel’s original event structure semantics of CCS.

I&C Journal 2009 Journal Article

Objects and session types

• Mariangiola Dezani-Ciancaglini
• Sophia Drossopoulou
• Dimitris Mostrous
• Nobuko Yoshida

A session takes place between two parties; after establishing a connection, each party interleaves local computations and communications (sending or receiving) with the other. Session types characterise such sessions in terms of the types of values communicated and the shape of protocols, and have been developed for the π -calculus, CORBA interfaces, and functional languages. We study the incorporation of session types into object-oriented languages through MOOSE, a multi-threaded language with session types, thread spawning, iterative, and higher-order sessions. Our design aims to consistently integrate the object-oriented programming style and sessions, and to be able to treat various case studies from the literature. We describe the design of MOOSE, its syntax, operational semantics, and type system, and develop a type inference system. After proving subject reduction, we establish the progress property: once a communication has been established, well-typed programs will never starve at communication points.

TCS Journal 2007 Journal Article

Formalising Java RMI with explicit code mobility

• Alexander Ahern
• Nobuko Yoshida

This paper presents an object-oriented, Java-like core language with primitives for distributed programming and explicit code mobility. We apply our formulation to prove the correctness of several optimisations for distributed programs. Our language captures crucial but often hidden aspects of distributed object-oriented programming, including object serialisation, dynamic class downloading and remote method invocation. It is defined in terms of an operational semantics that concisely models the behaviour of distributed programs using machinery from calculi of mobile processes. Type safety is established using invariant properties for distributed runtime configurations. We argue that primitives for explicit code mobility offer a programmer fine-grained control of type-safe code distribution, which is crucial for improving the performance and safety of distributed object-oriented applications.

TCS Journal 2006 Journal Article

Editorial

• Philippa Gardner
• Nobuko Yoshida

I&C Journal 2004 Journal Article

Strong normalisation in the π-calculus

• Nobuko Yoshida
• Martin Berger
• Kohei Honda

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.

I&C Journal 2002 Journal Article

Assigning Types to Processes

• Nobuko Yoshida
• Matthew Hennessy

In wide area distributed systems it is now common for higher-order code to be transferred from one domain to another; the receiving host may initialise parameters and then execute the code in its local environment. In this paper we propose a fine-grained typing system for a higher-order π-calculus which can be used to control the effect of such migrating code on local environments. Processes may be assigned different types depending on their intended use. This is in contrast to most of the previous work on typing processes where all processes are typed by a unique constant type, indicating essentially that they are well typed relative to a particular environment. Our fine-grained typing facilitates the management of access rights and provides host protection from potentially malicious behaviour. Our process type takes the form of an interface limiting the resources to which it has access and the types at which they may be used. Allowing resource names to appear both in process types and process terms, as interaction ports, complicates the typing system considerably. For the development of a coherent typing system, we use a kinding technique, similar to that used by the subtyping of the system F, and order-theoretic properties of our subtyping relation. Various examples of this paper illustrate the usage of our fine-grained process types in distributed systems.

TCS Journal 2002 Journal Article

Minimality and separation results on asynchronous mobile processes – representability theorems by concurrent combinators

• Nobuko Yoshida

In Honda and Yoshida (TACS’94, Lecture Notes in Computer Science, vol. 789, Springer, Berlin, 1994, pp. 786–805; POPL’94, ACM Press, New York, 1994, pp. 348–360) we presented a theory of concurrent combinators for the asynchronous monadic π-calculus without match or summation operator. The system of concurrent combinators is based on a finite number of atoms and fixed interaction rules, but is as expressive as the original calculus, so that it can represent diverse interaction structures, including polyadic synchronous name passing and input guarded summations. The present paper shows that each of the five basic combinators introduced in Honda and Yoshida (POPL’94, ACM Press, New York, 1994, pp. 348–360) is indispensable to represent the whole computation, i. e. if one of the combinators is missing, we can no longer express the original calculus up to semantic equalities. Expressive power of several interesting subsystems of the asynchronous π-calculus is also measured by using appropriate subsets of the combinators and their variants. Finally, as an application of the main result, we show there is no semantically sound encoding of the calculus into its proper subsystem under a certain condition.

TCS Journal 1999 Journal Article

Game-theoretic analysis of call-by-value computation

• Kohei Honda
• Nobuko Yoshida

We present a general semantic universe of call-by-value computation based on elements of game semantics, and validate its appropriateness as a semantic universe by the full abstraction result for call-by-value PCF, a generic typed programming language with call-by-value evaluation. The key idea is to consider the distinction between call-by-name and call-by-value as that of the structure of information flow, which determines the basic form of games. In this way the call-by-name computation and call-by-value computation arise as two independent instances of sequential functional computation with distinct algebraic structures. We elucidate the type structures of the universe following the standard categorical framework developed in the context of domain theory. Mutual relationship between the presented category of games and the corresponding call-by-name universe is also clarified.

TCS Journal 1995 Journal Article

On reduction-based process semantics

• Kohei Honda
• Nobuko Yoshida

A formulation of semantic theories for processes which does not rely on the notion of observables or convergence is studied. The new construction is based solely on a reduction relation and equational reasoning, but can induce meaningful theories for processes, both in weak and strong settings. The resulting theories in many cases coincide with, and sometimes generalise, observation-based formulation of behavioural equivalence. The basic construction of reduction-based theories is studied, taking a simple name passing calculus (called ν-calculus) and its extensions as an example. Results concerning the application of our construction to other calculi are also briefly discussed.