Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
I&C Journal 2005 Journal Article
A type system for terms of the monadic π-calculus is introduced and used to obtain a full-abstraction result for the translation of the polyadic π-calculus into the monadic calculus: well-sorted terms of the polyadic calculus are barbed congruent iff their translations are typed barbed congruent.
TCS Journal 1998 Journal Article
Transformation rules which increase the scope for concurrent activity within systems prescribed by programs of concurrent-object languages are given. Their correctness is proved on the basis of a semantic definition by translation to an extension of the π-calculus. The main theoretical development concerns the notions of confluence and partial confluence of processes.
TCS Journal 1998 Journal Article
A process calculus extending the π-calculus with higher-order agent abstractions as in the Higher-Order π-calculus and first-order data other than names but with only first-order interaction is used to give a natural and direct semantic definition for a concurrent object-oriented programming language. A notion of partial confluence of agents is introduced and its theory developed, first in the setting of CCS and then in the mobile-process calculus. It is shown how the semantic definition can be used as a basis for reasoning about systems prescribed by programs of the language: the theory of partial confluence is used to prove the indistinguishability in an arbitrary program context of two classes whose instances combine to form data structures only one of which supports concurrent operations.
TCS Journal 1993 Journal Article
In process algebras, bisimulation equivalence is typically defined directly in terms of the operational rules of action; it also has an alternative characterization in terms of a simple modal logic (sometimes called Hennessy-Milner logic). This paper first defines two forms of bisimulation equivalence for the π-calculus, a process algebra which allows dynamic reconfiguration among processes; it then explores a family of possible logics, with different modal operators. It is proven that two of these logics characterize the two bisimulation equivalences. Also, the relative expressive power of all the logics is exhibited as a lattice. The results are applicable to most value-passing process algebras.
I&C Journal 1992 Journal Article
We present the π-calculus, a calculus of communicating systems in which one can naturally express processes which have changing structure. Not only may the component agents of a system be arbitrarily linked, but a communication between neighbours may carry information which changes that linkage. The calculus is an extension of the process algebra CCS, following work by Engberg and Nielsen, who added mobility to CCS while preserving its algebraic properties. The π-calculus gains simplicity by removing all distinction between variables and constants; communication links are identified by names, and computation is represented purely as the communication of names across links. After an illustrated description of how the π-calculus generalises conventional process algebras in treating mobility, several examples exploiting mobility are given in some detail. The important examples are the encoding into the π-calculus of higher-order functions (the λ-calculus and combinatory algebra), the transmission of processes as values, and the representation of data structures as processes. The paper continues by presenting the algebraic theory of strong bisimilarity and strong equivalence, including a new notion of equivalence indexed by distinctions—i. e. , assumptions of inequality among names. These theories are based upon a semantics in terms of a labeled transition system and a notion of strong bisimulation, both of which are expounded in detail in a companion paper. We also report briefly on work-in-progress based upon the corresponding notion of weak bisimulation, in which internal actions cannot be observed.
I&C Journal 1992 Journal Article
This is the second of two papers in which we present the π-calculus, a calculus of mobile processes. We provide a detailed presentation of some of the theory of the calculus developed to date, and in particular we establish most of the results stated in the companion paper.
TCS Journal 1991 Journal Article