Nobuko Yoshida

Global Progress in Dynamically Merged Multiparty Sessions (2009)

Abstract. We propose an extension of Hennessy-Milner logic for the π-calculus which gives sound and complete characterisation of representative behavioural preorder and equivalence over typed...

Lorenzo Bettini, Marco De Luca, Mariangiola Dezani-ciancaglini, Nobuko Yoshida

Abstract. A multiparty session forms a unit of structured interactions among many participants which follow a prescribed scenario specified as a global type signature. This paper develops, besides a...

Global Principal Typing in Partially Commutative Asynchronous Sessions (2009)

Dimitris Mostrous, Nobuko Yoshida, Kohei Honda

Abstract. We generalise a theory of multiparty session types for the π-calculus through asynchronous communication subtyping, which allows partial commutativity of actions with maximal flexibility...

Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes (2009)

PLACES 2008 Synchronous Multiparty Session Types (2009)

Abstract. We study an extension of Hennessy-Milner logic for the π-calculus which gives a sound and complete characterisation of representative behavioural preorders and equivalences over typed...

Marco Carbone (2009)

Queen Mary, Nobuko Yoshida, Queen Mary

Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been studied over...

Andi Bejleri, Nobuko Yoshida

Synchronous communication is useful to model multiparty sessions where control for timing events and strong sequentially order of messages are essential to the problem specification. This paper...

Session Types for Object-Oriented Languages Dedicated to Giuseppe Longo at the occasion of his 60th birthday (2009)

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...

Global Progress in Dynamically Interleaved (2009)

Multiparty Sessions, Lorenzo Bettini, Marco De Luca, Mariangiola Dezani, Nobuko Yoshida

Widespread use of message-based communication for developing network applications to combine numerous distributed services has provoked urgent interest in structuring series of interactions to...

Molecular Mechanisms of TrypanosomaCruzi Infection by Oral Route (2009)

Yoshida, Nobuko

Frequent reports on outbreaks of acute Chagas’ disease by ingestion of food contaminated with parasites from triatomine insects illustrate the importance of this mode of transmission. Studies on...

Strong Normalisation in the p-Calculus \Lambda (2009)

Nobuko Yoshida, Martin Berger, Kohei Honda

Type-Directed Compilation for Multicore Programming Kohei Honda (2009)

Vasco T. Vasconcelos, Nobuko Yoshida

Preamble. In this abstract we outline a general picture of our ongoing work on compilation into multicore CPUs [8, 14, 15]. Our focus is to harness the power of concurrency and asynchrony in one of...

Local State in Imperative Higher-Order Programming. Local (2009)

Session-Based Distributed Programming in Java (2009)

We introduce an extension of Hoare logic for imperative higherorder functions with local state and full aliasing. Local state may be generated dynamically and exported outside its scope, may store...

Raymond Hu, Nobuko Yoshida

Abstract. This paper demonstrates the impact of integrating session types and object-oriented programming, through their implementation in Java. Session types provide high-level abstraction for...

Features (2008)

This paper demonstrates the impact of integrating session types for communication behaviour into object-oriented languages, through their implementation in a distributed Java. Session types abstract...

Probabilistic π-Calculus and Event Structures (2008)

Daniele Varacca, Nobuko Yoshida

This paper proposes two semantics of a probabilistic variant of the π-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event...

Under consideration for publication in J. Functional Programming 1 Short Note: Verification of In-Place List-Reversal with Effect Sets (2008)

Timed, Distributed, Probabilistic, Typed Processes (2008)

This short note presents a modular correctness proof of a simple in-place list reversal algorithm that is a stable of the relevant literature, cf. (Reynolds, 2002). To keep this note short, we assume...

Abstract A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

Abstract. This paper studies types and probabilistic bisimulations for a timed π-calculus as an effective tool for a compositional analysis of probabilistic distributed behaviour. The types clarify...

Martin Berger, Kohei Honda, Queen Mary, Nobuko Yoshida

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

Acta Informatica manuscript No. (2008)

Matthew Hennessy, Julian Rathke, Nobuko Yoshida

(will be inserted by the editor) safeDpi: a language for controlling mobile code ⋆

Logical Reasoning for Higher-Order Functions with Local State (2008)

Yoshida, Nobuko, Honda, Kohei, Berger, Martin

We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their...

Compositional Event Structure Semantics for the π-Calculus (2008)

Silvia Crafa, Daniele Varacca, Nobuko Yoshida

Abstract. We propose the first compositional event structure semantics for a fully expressive π-calculus, generalising Winskel’s event structures for CCS. The π-calculus we model is the...

Under consideration for publication in J. Functional Programming 1 A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

Mobile Programming with Ambients (2008)

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

Andrew Phillips, Susan Eisenbach, Nobuko Yoshida

Mobility is an important paradigm for modern distributed applications, where mobile code is supplied on demand and mobile components interact freely within a given network. However, mobile...

Bounded Session Types for Object Oriented Languages ⋆ (2008)

Mariangiola Dezani-ciancaglini, Elena Giachino, Sophia Drossopoulou, Nobuko Yoshida

Abstract. Earlier work explored the introduction of session types into object oriented languages. Following the session types literature, two parties would start communicating, provided the types...

Typed Event Structures and the π-Calculus – Extended Abstract – (2008)

Daniele Varacca, Nobuko Yoshida

Abstract. We propose a typing system for the true concurrent model of event structures that guarantees an interesting behavioural property known as confusion freeness. A system is confusion free if...

Abstract Logical Reasoning for Higher-Order Functions with Local State (2008)

Logics for Imperative Higher-Order Functions with Aliasing and Local State: Thee Completeness Results (2008)

We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their...

Abstract A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

Abstract. We establish three completeness properties (descriptive, relative and observational completeness) for the program logic for aliasing and higher-order functions, first studied in [1]. We...

Martin Berger, Kohei Honda, Queen Mary, Nobuko Yoshida

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

higher-order functions (2008)

Structured Global Programming for Communication (2008)

We present a compositional programme logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

Sequentiality and the ss-Calculus \Lambda (2008)

Abstract. This paper presents two different paradigms of description of communication behaviour, one focussing on global message flows and another on endpoint behaviours, as formal calculi based on...

Under consideration for publication in J. Functional Programming 1 A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2008)

y

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

y, Kohei Honda (2008)

Structured Global Programming for Communication Behaviour Marco Carbone 1,2 Kohei Honda 1 (2008)

z

Structured Global Programming for Communication (2008)

Abstract. This paper presents two different paradigms of description of communication behaviour, one focussing on global message flows and another on endpoint behaviours, as formal calculi based on...

of Computation]: Semantics of Programming Languages (2008)

Abstract. This paper presents two different paradigms of description of communication behaviour, one focussing on global message flows and another on endpoint behaviours, as formal calculi based on...

Er Ahern, Nobuko Yoshida

This paper presents a Java-like core language with primitives for object-oriented distribution and explicit code mobility. We apply our formulation to prove the correctness of several optimisations...

Program Logic and Program Analysis (2008)

Multiparty asynchronous session types (2008)

One of the central merits of compositional program logics [18] as a foundation of software engineering is their potential ability to describe a large class of properties of programs relative to a...

Kohei Honda, Nobuko Yoshida, Marco Carbone

Abstract. Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-based programming, session types have been...

Communication-cEntric Software (2008)

Vasco T. Vasconcelos, Nobuko Yoshida, Vasco T. Vasconcelos, Nobuko Yoshida

Technical reports are available at

Global Progress in Dynamically Interleaved Multiparty Sessions (2008)

Lorenzo Bettini, Marco De Luca, Mariangiola Dezani-ciancaglini, Nobuko Yoshida

Abstract. A multiparty session forms a unit of structured interactions among many participants which follow a prescribed scenario specified as a global type signature. This paper develops, besides a...

Multiparty Asynchronous Session Types (2008)

Kohei Honda, Nobuko Yoshida, Andi Bejleri, Marco Carbone

Abstract. Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been...

A Session Object Calculus for Structured CommunicationBased Programming (2008)

Dimitris Mostrous, Nobuko Yoshida

We present an object calculus for structured concurrent programming, facilitating the implementation of typed binary protocols, known as sessions. Session types are based on a concept of duality of...

Session-based distributed programming in Java (2008)

Sequentiality and the Pi Calculus (2007)

Abstract. This paper demonstrates the impact of integrating session types and object-oriented programming, through their implementation in Java. Session types provide high-level abstraction for...

Abstract. We present a simple type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The...

Processes, Types and Information Flow (2007)

Abstract. We present a simple type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The...

Specification techniques (2007)

. We develop a behavioural theory of secure information ow using a typed -calculus as a metalanguage, and show its applicability to the analysis and reasoning of secrecy concerns in programming...

Queen Mary London, Nobuko Yoshida

This paper introduces a compositional program logic for higherorder polymorphic functions and standard data types. The logic enables us to reason about observable properties of polymorphic programs...

Abstract. We present a simple type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The...

Nobuko Yoshida, Mario Tokoro

This paper gives basic definitions of f-calculus. f-calculus is a variant of-calculus which represents functional computation with shared environments. The formalism has a Church Rosser property and...

, Kohei Honda (2007)

Abstract.. We present a type discipline for the -calculus which precisely captures the notion of sequential functional computation as a specic class of name passing interactive behaviour. The typed...

Abstract. We present a type discipline for the -calculus which precisely captures the notion of sequential functional computation as a speci c class of name passing interactive behaviour. The typed...

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Sequentiality and the r-calculus (2007)

Abstract. We introduce a second-order polymorphic -calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of signicant technical...

Abstract. We introduce a second-order polymorphic r-calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of significant technical...

and Kohei Honda (2007)

Vasco Vasconcelos, Nobuko Yoshida

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Kohei Honda 1 (2007)

Abstract. We propose a new type discipline for the -calculus in which secure information ow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by...

and Kohei Honda (2007)

Reduction Theories for Concurrent Calculi (2007)

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Nobuko Yoshida, Kohei Honda

A formulation of semantic theories for processes which does not rely on the notion of observables or convergence, is studied. The new construction is solely based on reduction relation and equational...

Dynamic Channel Screening in the Higher Order -Calculus (2007)

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Jose Luis Vivas, Nobuko Yoshida

Abstract. Recently programming languages have been designed to support mobile code, i.e. higher-order code that is transferred from a remote location or domain and executed within the local...

A Uniform Type Structure for Secure Information Flow Kohei Honda Deptartment of Computer Science (2007)

Queen Mary, Nobuko Yoshida

The -calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name...

Noninterference Proofs through Flow Analysis (2007)

Abstract. We introduce a theory of weak bisimilarity for the -calculus with linear type structure [35] in which we abstract away not only -actions but also non- actions which do not aect well-typed...

Noninterference Proofs through Flow Analysis (2007)

This note proves noninterference results (NI) for the secrecy analyses for LA and WLAU presented in [1], using the inductive information flow analysis. This flow analysis is related to the secrecy...

Abstract. Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the -calculus in which we abstract away not only -actions but also non- actions which do not aect...

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Co-infection with Trypanosoma cruziprotects mice against early death by neurological or pulmonary disorders induced by Plasmodium bergheiANKA (2007)

We introduce a typed p-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite...

Egima, Claudia M, Macedo, Silene F, Sasso, Gisela RS, Covarrubias, Charles, Cortez, Mauro, Maeda, Fernando Y, ...

Abstract Objective The objective of this study was to investigate whether the infection of C57BL/6 mice by P. berghei ANKA, which causes severe malaria, was modulated by co-infection with Trypanosoma...

Compositional Event Structure Semantics of the Internal pi-Calculus (2007)

Crafa, Silvia, Varacca, Daniele, Yoshida, Nobuko

We propose the ﬁrst compositional event structure semantics for a fully expressive pi-calculus, generalising Winskel's event structures for CCS. The pi-calculus we model is the piI-calculus...

Probabilistic pi-calculus and Event Structures (2007)

Varacca, Daniele, Yoshida, Nobuko

This paper proposes two semantics of a probabilistic variant of the pi-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event...

Compositional Event Structure Semantics of the Internal pi-Calculus (2007)

Crafa, Silvia, Varacca, Daniele, Yoshida, Nobuko

We propose the ﬁrst compositional event structure semantics for a fully expressive pi-calculus, generalising Winskel's event structures for CCS. The pi-calculus we model is the piI-calculus...

Probabilistic pi-calculus and Event Structures (2007)

Varacca, Daniele, Yoshida, Nobuko

This paper proposes two semantics of a probabilistic variant of the pi-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event...

Language and Runtime Implementation of Sessions for Java (2007)

Structured Communication-Centred Programming for Web Services (2007)

The purpose of this work is to incorporate the principles of session types into a

Language and Runtime Implementation of Sessions for Java (2007)

Abstract. This paper relates two different paradigms of descriptions of communication behaviour, one focussing on global message flows and another on end-point behaviours, using formal calculi based...

Transfer Report Wildcards, Variance and Virtual Classes (2007)

The purpose of this work is to incorporate the principles of session types into a

Nick Cameron, Supervised Sophia Drossopoulou, Nobuko Yoshida

Wildcards are used in Java to soften the mismatch between parametric polymorphism (generics) and subtype polymorphism (inheritance). Java with wildcards has not been proven type sound (unlike...

Local state in hoare logic for imperative higher-order functions (2007)

Local state in hoare logic for imperative higher-order functions (2007)

Abstract. We introduce an extension of Hoare logic for imperative higher-order functions with local state. Local state may be generated dynamically and exported outside its scope, may store...

Two session typing systems for higher-order mobile processes (2007)

Abstract. We introduce an extension of Hoare logic for imperative higher-order functions with local state. Local state may be generated dynamically and exported outside its scope, may store...

Dimitris Mostrous, Nobuko Yoshida

Abstract. This paper proposes two typing systems for session interactions in higherorder mobile processes. Session types for the HOπ-calculus capture high-level structures of communication protocols...

On Progress for Structured Communications (2007)

Mariangiola Dezani-ciancaglini, Ugo De Liguoro, Nobuko Yoshida

Abstract. We propose a new typing system for the π-calculus with sessions, which ensures the progress property, i.e. once a session has been initiated, typable processes will never starve at session...

Asynchronous Session Types and Progress for Object-Oriented Languages (2007)

Mariangiola Dezani-ciancaglini, Nobuko Yoshida

Abstract. A session type is an abstraction of a sequence of heterogeneous values sent over one channel between two communicating processes. Session types have been introduced to guarantee consistency...

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other. Session...

A Calculus of Global Interaction Based on Session Types (2006)

Logical reasoning for higher-order functions with local state (2006)

This paper proposes a calculus for describing communication-centred programming and discusses its application to use cases from real business protocols. The formalism, called global calculus, aims at...

Nobuko Yoshida, Kohei Honda, Martin Berger, Queen Mary

Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Logical reasoning for higher-order functions with local state (2006)

Typed event Structures and the π-calculus (2006)

Abstract. We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Daniele Varacca, Nobuko Yoshida

Abstract. We propose a typing system for the true concurrent model of event structures that guarantees an interesting behavioural property known as confusion freeness. A system is confusion free if...

Logical reasoning for higher-order functions with local state (2006)

Nobuko Yoshida, Kohei Honda, Martin Berger, Queen Mary

Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other party....

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a con-nection, each interleaves local computations and communications (sending or receiving) with the other. Session types...

Logical reasoning for higher-order functions with local state (2006)

Descriptive and relative completeness for logics for higher-order functions (2006)

Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Kohei Honda, Martin Berger, Nobuko Yoshida

Abstract. This paper establishes a strong completeness property of compositional program logics for pure and imperative higher-order functions introduced in [2, 15–18]. This property, called...

Logical reasoning for higher-order functions with local state (2006)

Abstract. We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside...

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other. Session...

safeDpi: a language for controlling mobile code (2005)

Hennessy, Matthew, Yoshida, Nobuko, Rathke, Julian

safeDpi is a distributed version of the Picalculus, in which processes are located at dynamically created sites. Parametrised code may be sent between sites using so-called ports, which are...

safeDpi: a language for controlling mobile code (2005)

Hennessy, Matthew, Yoshida, Nobuko, Rathke, Julian

safeDpi is a distributed version of the Picalculus, in which processes are located at dynamically created sites. Parametrised code may be sent between sites using so-called ports, which are...

safeDpi: a language for controlling mobile code (2005)

Hennessy, Matthew, Yoshida, Nobuko, Rathke, Julian

safeDpi is a distributed version of the Picalculus, in which processes are located at dynamically created sites. Parametrised code may be sent between sites using so-called ports, which are...

An observationally complete program logic for imperative higher-order functions (2005)

An observationally complete program logic for imperative higher-order functions (2005)

Abstract. We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order...

A Distributed Object-Oriented Language with Session Types (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

A Distributed Object-Oriented Language with Session Types (2005)

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

An Observationally Complete Program Logic for Imperative Higher-Order Functions (2005)

A Distributed Object-Oriented Language with Session Types (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

An Observationally Complete Program Logic for Imperative Higher-Order Functions (2005)

Synchronisation for DJ (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

Alexander Ahern, Er Ahern, Nobuko Yoshida, Er Ahern, Nobuko Yoshida

The function og(s , v) computes the object graph of value v in store s . This is defined as the set of all mappings from object identifier to store object for every local object transitively...

A Logical Analysis of Aliasing in Imperative Higher-Order Functions (2005)

A Distributed Object-Oriented Language with Session Types (2005)

We present a compositional program logic for call-by-value imperative higherorder functions with general forms of aliasing, which can arise from the use of reference names as function parameters,...

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

A logical analysis of aliasing in imperative higher-order functions (2005)

An observationally complete program logic for imperative higher-order functions (2005)

Abstract. We present a compositional program logic for call-by-value imperative higherorder functions with general forms of aliasing, which can arise from the use of reference names as function...

An observationally complete program logic for imperative higher-order functions (2005)

We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A...

SafeDpi: a language for controlling mobile code (2004)

Abstract. We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order...

Hennessy, Matthew, Rathke, Julian, Yoshida, Nobuko

Channel dependency types for higher-order mobile processes (2004)

A distributed abstract machine for boxed ambient calculi (2004)

We introduce a new expressive theory of types for the higher-order p-calculus and demonstrate its applicability via non-trivial security analyses of a simple class-based language with distributed...

Andrew Phillips, Nobuko Yoshida, Susan Eisenbach

Channel Dependent Types for Higher-Order Mobile Processes (Extended Abstract) (2004)

Channel Dependent Types for Higher-Order Mobile Processes (Part I) (2004)

Nobuko Yoshida Imperial College London ABSTRACT We introduce a new expressive theory of types for the higher-order p-calculus and demonstrate its applicability via non-trivial security analyses of a...

Formal Analysis of a Distributed Object-Oriented Language and Runtime (2004)

We introduce a new expressive theory of types for the higher-order p-calculus which significantly improves our previous work presented in [65] by the use of channel dependent/existential types. New...

Alexander Ahern, Er Ahern, Nobuko Yoshida

Distributed language features form an important part of modern objectoriented programming. In spite of their prominence in today's computing environments, the formal semantics of distributed...

A distributed abstract machine for boxed ambient calculi (2004)

Andrew Phillips, Nobuko Yoshida, Susan Eisenbach

A Compositional Logic for Polymorphic Higher-Order Functions (2004)

Queen Mary London, Nobuko Yoshida

This paper introduces a compositional program logic for higherorder polymorphic functions and standard data types. The logic enables us to reason about observable properties of polymorphic programs...

SafeDpi: a language for controlling mobile code (2003)

Hennessy, Matthew, Rathke, Julian, Yoshida, Nobuko

SafeDPi: A language for controlling mobile code (2003)

Matthew Hennessy, Julian Rathke, Nobuko Yoshida

Abstract. safeDpi is a distributed version of the Picalculus, in which processes are located at dynamically created sites. Parametrised code may be sent between sites using so-called ports, which are...

Genericity and the π-Calculus (2003)

safeDpi: a language for controlling mobile code (2003)

Types in processes delineate specific classes of interactive behaviour in a compositional way. Key elements of process theory, in particular behavioural equivalences, are deeply affected by types,...

Matthew Hennessy, Julian Rathke, Nobuko Yoshida

safeDpi is a distributed version of the Picalculus, in which processes are located at dynamically created sites. Parametrised code may be sent between sites using so-called ports, which are...

Linearity and bisimulation (2002)

Type-Based Liveness Guarantee in the Presence of Nontermination and Nondeterminism (2002)

Abstract. Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not...

A Uniform Type Structure for Secure Information Flow (2002)

Abstract. This paper investigates a type-based framework to guarantee a basic liveness property in the -calculus. The resulting liveness property ensures that the action at a specied channel will...

Sequentiality and the π-calculus (2001)

The -calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name...

Sequentiality and the -calculus (2001)

We introduce a second-order polymorphic π-calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of significant technical...

Sequentiality and the -calculus (2001)

Abstract. We introduce a second-order polymorphic -calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of signicant technical...

Assigning types to processes (2000)

Abstract. Types in processes delineate specic classes of interactive behaviour in a compositional way. Key elements of process theory, in particular behavioural equivalences, are deeply aected by...

Assigning types to processes (2000)

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...

Assigning Types to Processes (2000)

ABSTRACT. 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...

Assigning Types to Processes (Extended Abstract) (2000)

. 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...

Secure Information Flow as Typed Process Behaviour (2000)

) NOBUKO YOSHIDA MATTHEW HENNESSY Dept. of Mathematics and Computer Science School of Cognitive and Computing Sciences University of Leicester Univerrsiry of Sussex ABSTRACT In wide area distributed...

Secure Information Flow as Typed Process Behaviour (2000)

. We propose a new type discipline for the #-calculus in which secure information flow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping....

Secure Information Flow as Typed Process Behaviour (2000)

. We propose a new type discipline for the pi-calculus in which secure information ow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping. A...

Secure Information Flow as Typed Process Behaviour (2000)

We propose a new type discipline for the pi-calculus in which secure information ow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping. A...

Assigning Types to Processes (Extended Abstract) (2000)

. We propose a new type discipline for the #-calculus in which secure information flow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping....

RESEARCH NOTE - Heterologous Expression of a Trypanosoma cruzi Surface Glycoprotein (gp82) Indicates that Requirements for Glycosylphosphatidyl-inositol Anchoring are Different in Mammalian Cells and this Trypanosome (1999)

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...

Marcel I Ramirez, Silvia B Boscardin, Rita C Ruiz, Sang W Han, Nobuko Yoshida, ...

Metacyclic trypomastigotes of Trypanosoma cruzi express a stage-specific surface glycoprotein of 82 kDa (gp82) which has been implicated in the invasion of the mammalian host cells

Organization and Expression of a Multigene Family Encoding the Surface Glycoproteins of Trypanosoma cruzi Metacyclic Trypomastigotes Involved in the Cell Invasion (1999)

Mirian S Carmo, Jorge E Araya, Marcel I Ramirez, Silvia Boscardin, Maria I Cano, Renata P Baida, ...

Organization and expression of a multigene family encoding the surface glycoproteins of Trypanosoma cruzi metacyclic trypomastigotes involved in the cell invasion (1999)

Carmo,Mirian S, Araya,Jorge E, Ramirez,Marcel I, Boscardin,Silvia, Cano,Maria I, Baida,Renata P, ...

Heterologous Expression of a Trypanosoma cruzi Surface Glycoprotein (gp82) Indicates that Requirements for Glycosylphosphatidylinositol Anchoring are Different in Mammalian Cells and this Trypanosome (1999)

Ramirez,Marcel I, Boscardin,Silvia B, Ruiz,Rita C, Han,Sang W, Paranhos-Baccala,Glaucia S, Yoshida,Nobuko, ...

Subtyping and Locality in Distributed Higher Order Processes (Extended Abstract) (1999)

Subtyping and Locality in Distributed Higher Order Processes (1999)

. This paper studies one important aspect of distributed systems, locality, using a calculus of distributed higher-order processes in which not only basic values or channels, but also parameterised...

Extended Nobuko, Nobuko Yoshida, Matthew Hennessy

. This paper studies one important aspect of distributed systems, locality, using a calculus of distributed higher-order processes in which not only basic values or channels, but also parameterised...

Subtyping and Locality in Distributed Higher Order Processes (1999)

Language primitives and type discipline for structured communication-based programming (1998)

: This paper studies one important aspect of distributed systems, locality, using a calculus of distributed higher-order processes in which not only basic values or channels, but also parameterised...

Nobuko Yoshida, Vasco T. Vasconcelos

Session primitives and types provide a flexible programming style for structured interaction, and are used to statically check the safe and consistent composition of protocols in...

Minimality and Separation Results on Asynchronous Mobile Processes - Representability Theorems by Concurrent Combinators (Extended Abstract) (1998)

Minimality and Separation Results on Asynchronous Mobile Processes - Representability Theorems by Concurrent Combinators (1998)

) y Nobuko Yoshida ? Abstract. In [18, 19], we presented a theory of concurrent combinators for the asynchronous monadic ß-calculus without match or summation operator [7, 16]. The system of...

Minimality and Separation Results on Asynchronous Mobile Processes - Representability Theorem by Concurrent Combinators (1998)

. In [22, 23], we presented a theory of concurrent combinators for the asynchronous monadic ß-calculus without match or summation operator [7, 19]. The system of concurrent combinators is based on a...

N. Yoshida, Nobuko Yoshida

. In [15, 16], we presented a theory of concurrent combinators for the asynchronous monadic ß-calculus without match or summation operator [13, 6]. The system of concurrent combinators is based on a...

Language primitives and type discipline for structured communication-based programming (1998)

Vasco T. Vasconcelos, Nobuko Yoshida

available by post from the above address.

Language primitives and type disciplines for structured communication-based programming (1998)

Vasco T. Vasconcelos, Nobuko Yoshida

available by post from the above address.

GRAPH TYPES FOR MONADIC MOBILE PROCESSES(Concurrency Theory and Applications '96) (1997)

YOSHIDA, NOBUKO

Game Theoretic Analysis Of Call-By-Value Computation (1997)

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...

Game Theoretic Analysis Of Call-By-Value Computation (1997)

Game Theoretic Analysis Of Call-By-Value Computation (1997)

. 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...

Explicit Code Mobility in Java RMI (1997)

. 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...

Alexander Ahern, N. Yoshida, Er Ahern, Nobuko Yoshida, Drossopoulou Eisenbach

REFERENCES

Graph Types For Monadic Mobile Processes (1996)

Graph Types For Monadic Mobile Processes (1996)

. While types for name passing calculi have been studied extensively in the context of sorting of polyadic ß-calculus [5, 34, 9, 28, 32, 19, 33, 10, 17], the same type abstraction is not possible in...

Graph Types For Monadic Mobile Processes (1996)

. While types for name passing calculi have been studied extensively in the context of sorting of polyadic ß-calculus [26, 7, 43, 11, 35, 41, 24, 42, 14, 22], the type abstraction on the...

Graph types for monadic mobile processes (1996)

Encoding for Polyadic -calculus This section establishes the full abstraction result for the standard encoding of polyadic -calculus into monadic -calculus in terms of a basic behavioural equality in...

On Reduction-Based Process Semantics (1995)

While types for name passing calculi have been studied extensively in the context of

Honda, Kohei, Yoshida, Nobuko

On reduction-based process semantics (1995)

On Reduction-Based Process Semantics (1995)

Abstract. A formulation of semantic theories for processes which is based on reduction relation and equational reasoning is studied. The new construction can induce meaningful theories for processes,...

Graph Notation For Concurrent Combinators (1995)

A formulation of semantic theories for processes which is based on reduction relation and equational reasoning is studied. The new construction can induce meaningful theories for processes, both in...

On Reduction-Based Process Semantics (1995)

. We introduce graph notation for concurrent processes which does not use the notion of port names for its formulation. The operators in the algebra of graphs proposed in this paper are quite...

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...

Combinatory Representation of Mobile Processes (1994)

Replication in Concurrent Combinators (1994)

A possible analogue of theory of combinators in the setting of concurrent processes is formulated. The new combinators are derived from the analysis of the operation called asynchronous name passing,...