We propose an Operational Game Semantics for a (call-by-value) concurrent higher-order language with first-order store (references may contain other references or first-order values such as integers or booleans; however they may not store higher-order values such as functions). We adapt the game-semantic notion of visibility, which semantically captures the absence of higher-order references and developed for sequential higher-order languages, to a concurrent setting. We thus define a complete-trace preorder, and prove it sound for the contextual preorder, by introducing a synchronization-based composition of semantic configurations and establishing an observational adequacy result. We also prove completeness for the subset of the language in which functions return first-order values. In contrast to the case of sequential visibility, in the labeled transition semantics we have to account for the presence of multiple active threads with possibly different visibilities, and of a tree-like structure for managing the dependencies among the threads so created. Moreover, we have to reason on families of traces, rather than single traces, as in concurrent setting the order among certain actions cannot be enforced.

The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed.

Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $λ$-calculus, the process representations yield (at best) non-extensional $λ$-theories (i.e., $β$ rule holds, whereas $η$ does not). In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal $π$, $\mathrm{I}π$ (a subset of the $π$-calculus in which all outputs are bound), we develop a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a $λ$-theory. Exploiting the symmetries and dualities of $\mathrm{I}π$, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional $λ$-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite $η$. In contrast, the other two classes of wires yield non-extensional $λ$-theories whose equalities are those of the Lévy-Longo and Böhm trees.

Following Milner’s seminal paper, the representation of functions as processes has received considerable attention. For pure λ-calculus, the process representations yield (at best) non-extensional λ-theories (i.e., β rule holds, whereas η does not).In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal π, Iπ (a subset of the π-calculus in which all outputs are bound), we develop a refinement of Milner’s original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a λ-theory. Exploiting the symmetries and dualities of Iπ, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional λ-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite η. In contrast, the other two classes of wires yield non-extensional λ-theories whose equalities are those of the Lévy-Longo and Böhm trees.

This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four papers that received the Award in 2022.

Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order programming languages. However, due to the complexity of most game models, game semantics has remained unapproachable for non-experts. In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation into a session typed pi-calculus, referred to as metalanguage, followed by a semantics interpretation of the metalanguage into a particular game model. The syntactic translation can be defined for a wide range of programming languages without knowledge of the particular game model used. Simple reasoning on the model (soundness, and adequacy) can be done at the level of the metalanguage, escaping tedious technical proofs usually found in game semantics. We call this methodology programming game semantics. We design a metalanguage (PiDiLL) inspired from Differential Linear Logic (DiLL), which is concise but expressive enough to support features required by concurrent game semantics. We then demonstrate our methodology by yielding the first causal, non-angelic and interactive game model of CML, a higher-order call-by-value language with shared memory concurrency. We translate CML into PiDiLL and show that the translation is adequate. We give a causal and non-angelic game semantics model using event structures, which supports a simple semantics interpretation of PiDiLL. Combining both of these results, we obtain the first interactive model of a concurrent language of this expressivity which is adequate with respect to the standard weak bisimulation, and fully abstract for the contextual equivalence on second-order terms. We have implemented a prototype which can explore the generated causal object from a subset of OCaml.

International audience

There exist a rich and well-developed theory of enhancements of the coinduction proof method, widely used on behavioural relations such as bisimilarity. We study how to develop an analogous theory for inductive behaviour relations, i.e., relations defined from inductive observables. Similarly to the coinductive setting, our theory makes use of (semi)-progressions of the form R->F(R), where R is a relation on processes and F is a function on relations, meaning that there is an appropriate match on the transitions that the processes in R can perform in which the process derivatives are in F(R). For a given preorder, an enhancement corresponds to a sound function, i.e., one for which R->F(R) implies that R is contained in the preorder; and similarly for equivalences. We introduce weights on the observables of an inductive relation, and a weight-preserving condition on functions that guarantees soundness. We show that the class of functions contains non-trivial functions and enjoys closure properties with respect to desirable function constructors, so to be able to derive sophisticated sound functions (and hence sophisticated proof techniques) from simpler ones. We consider both strong semantics (in which all actions are treated equally) and weak semantics (in which one abstracts from internal transitions). We test our enhancements on a few non-trivial examples.

The $\pi$-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. In this paper we focus on two such common disciplines: sequentiality, meaning that at any time there is a single thread of computation, and well-bracketing, meaning that calls to external services obey a stack-like discipline. We formalise the disciplines by means of type systems. The main focus of the paper is on studying the consequence of the disciplines on behavioural equivalence. We define and study labelled bisimilarities for sequentiality and well-bracketing. These relations are coarser than ordinary bisimilarity. We prove that they are sound for the respective (contextual) barbed equivalence, and also complete under a certain technical condition. We show the usefulness of our techniques on a number of examples, that have mainly to do with the representation of functions and store.

The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.

The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been fully investigated. In this paper we address this issue. We focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We first define π^ref, an extension of Aπ with references and operators to manipulate them, and illustrate examples of the subtleties of behavioural equivalence in π^ref. We then consider a translation of π^ref into Aπ. References of π^ref are mapped onto names of Aπ belonging to a dedicated "reference" type. We show how the presence of reference names affects the definition of barbed congruence. We establish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the two calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another, more efficient and involving an inductive "game" on reference names, we derive soundness, leaving completeness open. Finally, we discuss examples of uses of the bisimilarities.

Abstract Bisimulation is an instance of coinduction. Both bisimulation and coinduction are today widely used, in many areas of Computer Science, as well as outside Computer Science. Over, roughly, the last 25 years, enhancements of the principles and methods related to bisimulation and coinduction (i.e., techniques to make proofs shorter and simpler) have become a research topic on its own. In the paper the origins and the developments of the topic are reviewed.

We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the `up-to techniques'). Finally, we study the theorems in name-passing calculi such as the asynchronous $\pi$-calculus, and use them to revisit the completeness part of the proof of full abstraction of Milner's encoding of the $\lambda$-calculus into the $\pi$-calculus for L\'evy-Longo Trees. Comment: This is an extended version of the paper with the same title published in the proceedings of CONCUR'17

Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ-calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case, full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as “up-to techniques,” are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.

We study Milner's encoding of the call-by-value λ-calculus into the π-calculus. We show that, by tuning the encoding to two subcalculi of the π-calculus (Internal π and Asynchronous Local π), the equivalence on λ-terms induced by the encoding coincides with Lassen's eager normal-form bisimilarity, extended to handle η-equality. As behavioural equivalence in the π-calculus we consider contextual equivalence and barbed congruence. We also extend the results to preorders.

Open bisimilarity is a strong bisimulation congruence for the pi-calculus. In open bisimilarity, free names in processes are treated as variables that may be instantiated; in contrast to late bisimilarity where free names are constants. An established modal logic due to Milner, Parrow, and Walker characterises late bisimilarity, that is, two processes satisfy the same set of formulae if and only if they are bisimilar. We propose an intuitionistic variation of this modal logic and prove that it characterises open bisimilarity. The soundness proof is mechanised in Abella. The completeness proof provides an algorithm for generating distinguishing formulae, useful for explaining and certifying whenever processes are non-bisimilar.

Session types are a formalism used to model structured communication-based programming. A binary session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session processes are added to the syntax of standard π-calculus they give rise to additional separate syntactic categories. As a consequence, when new type features are added, there is duplication of effort in the theory: the proofs of properties must be checked both on standard types and on session types. We show that session types are encodable into standard π-types, relying on linear and variant types. Besides being an expressivity result, the encoding (i) removes the above redundancies in the syntax, and (ii) the properties of session types are derived as straightforward corollaries, exploiting the corresponding properties of standard π-types. The robustness of the encoding is tested on a few extensions of session types, including subtyping, polymorphism and higher-order communications.

One of the most studied behavioural equivalences is bisimilarity. Its success is much due to the associated bisimulation proof method, which can be further enhanced by means of “bisimulation up-to” techniques such as “up-to context.” A different proof method is discussed, based on a unique solution of special forms of inequations called contractions and inspired by Milner’s theorem on unique solution of equations. The method is as powerful as the bisimulation proof method and its “up-to context” enhancements. The definition of contraction can be transferred onto other behavioural equivalences, possibly contextual and non-coinductive. This enables a coinductive reasoning style on such equivalences, either by applying the method based on unique solution of contractions or by injecting appropriate contraction preorders into the bisimulation game. The techniques are illustrated in CCS-like languages; an example dealing with higher-order languages is also shown.

Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ- calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as ‘up-to techniques’, are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.

We show that the techniques for resource control that have been developed by the so-calledlight logicscan be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

One of the most studied behavioural equivalences is bisimilarity. Its success is much due to the associated bisimulation proof method, which can be further enhanced by means of "up-to bisimulation" techniques such as "up-to context".

Objects and services are pervasive concepts in modern distributed systems. Objects and services, sometimes generically referred to as components, represent the unit of interaction. They offer mechanisms for abstraction and encapsulation, through a well-defined interface that specifies the way in which a given component can be used from the outside, thus hiding the details of the internal implementation. These features are important for building flexible systems, in which components can be used just by inspecting their interface.

We study bisimulation and context equivalence in a probabilistic lambda-calculus. The contributions of this paper are threefold. Firstly we show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. Secondly we show that, while bisimilarity is in general strictly finer than context equivalence, coincidence between the two relations is attained on pure lambda-terms. The resulting equality is that induced by Levy-Longo trees, generally accepted as the finest extensional equivalence on pure lambda-terms under a lazy regime. Finally, we derive a coinductive characterisation of context equivalence on the whole probabilistic language, via an extension in which terms akin to distributions may appear in redex position. Another motivation for the extension is that its operational semantics allows us to experiment with a different congruence technique, namely that of logical bisimilarity.

The fusion calculi are a simplification of the pi-calculus in which input and output are symmetric and restriction is the only binder. We highlight a major difference between these calculi and the pi-calculus from the point of view of types, proving some impossibility results for subtyping in fusion calculi. We propose a modification of fusion calculi in which the name equivalences produced by fusions are replaced by name preorders, and with a distinction between positive and negative occurrences of names. The resulting calculus allows us to import subtype systems, and related results, from the pi-calculus. We examine the consequences of the modification on behavioural equivalence (e.g., context-free characterisations of barbed congruence) and expressiveness (e.g., full abstraction of the embedding of the asynchronous pi-calculus).

Session types are a formalism to model structured communication-based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session primitives are added to the syntax of standard π-calculus types and terms, they give rise to additional separate syntactic categories. As a consequence, when new type features are added, there is duplication of efforts in the theory: the proofs of properties must be checked both on ordinary types and on session types. We show that session types are encodable in ordinary π types, relying on linear and variant types. Besides being an expressivity result, the encoding (i) removes the above redundancies in the syntax, and (ii) the properties of session types are derived as straightforward corollaries, exploiting the corresponding properties of ordinary π types. The robustness of the encoding is tested on a few extensions of session types, including subtyping, polymorphism and higher-order communications.

Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, as well as enhancements of the bisimulation proof method with “up-to context” techniques, and (2) obtaining definitions and results that scale to languages with different features. To meet these challenges, we present environment{} bisimulations , a form of bisimulation for higher-order languages, and its basic theory. We consider four representative calculi: pure λ-calculi (call-by-name and call-by-value), call-by-value λ-calculus with higher-order store, and then Higher-Order π-calculus. In each case: we present the basic properties of environment bisimilarity, including congruence; we show that it coincides with contextual equivalence; we develop some up-to techniques, including up-to context, as examples of possible enhancements of the associated bisimulation method. Unlike previous approaches (such as applicative bisimulations, logical relations, Sumii-Pierce-Koutavas-Wand), our method does not require induction/indices on evaluation derivation/steps (which may complicate the proofs of congruence, transitivity, and the combination with up-to techniques), or sophisticated methods such as Howe's for proving congruence. It also scales from the pure λ-calculi to the richer calculi with simple congruence proofs.

We propose a type system for lock-freedom in the π-calculus, which guarantees that certain communications will eventually succeed. Distinguishing features of our type system are: it can verify lock-freedom of concurrent programs that have sophisticated recursive communication structures; it can be fully automated; it is hybrid, in that it combines a type system for lock-freedom with local reasoning about deadlock-freedom, termination, and confluence analyses. Moreover, the type system is parameterized by deadlock-freedom/termination/confluence analyses, so that any methods (e.g. type systems and model checking) can be used for those analyses. A lock-freedom analysis tool has been implemented based on the proposed type system, and tested for nontrivial programs.

The origins of bisimulation and bisimilarity are examined, in the three fields where they have been independently discovered: Computer Science, Philosophical Logic (precisely, Modal Logic), Set Theory. Bisimulation and bisimilarity are coinductive notions, and as such are intimately related to fixed points, in particular greatest fixed points. Therefore also the appearance of coinduction and fixed points is discussed, though in this case only within Computer Science. The paper ends with some historical remarks on the main fixed-point theorems (such as Knaster-Tarski) that underpin the fixed-point theory presented.

In higher-order process calculi the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a nearly deterministic encoding of Minsky machines, the calculus is shown to be Turing complete and therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Further, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.

The \it{Ambient Logic} (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the discriminating power of AL, focusing on the equivalence on processes induced by the logic $(=_L>)$. As underlying calculi besides MA we consider a subcalculus in which an image-finiteness condition holds and that we prove to be Turing complete. Synchronous variants of these calculi are studied as well. In these calculi, we provide two operational characterisations of $_=L$: a coinductive one (as a form of bisimilarity) and an inductive one (based on structual properties of processes). After showing $_=L$ to be stricly finer than barbed congruence, we establish axiomatisations of $_=L$ on the subcalculus of MA (both the asynchronous and the synchronous version), enabling us to relate $_=L$ to structural congruence. We also present some (un)decidability results that are related to the above separation properties for AL: the undecidability of $_=L$ on MA and its decidability on the subcalculus.

Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, as well as enhancements of the bisimulation proof method with "up-to context" techniques, and (2) obtaining definitions and results that scale to languages with different features. To meet these challenges, we present environmental bisimulations, a form of bisimulation for higher-order languages, and its basic theory. We consider four representative calculi: pure lambda-calculi (call-by-name and call-by-value), call-by-value lambda-calculus with higher-order store, and then higher-order pi-calculus. In each case: we present the basic properties of environmental bisimilarity, including congruence; we show that it coincides with contextual equivalence; we develop some up-to techniques, including up-to context, as examples of possible enhancements of the associated bisimulation method. Unlike previous approaches (such as applicative bisimulations, logical relations, Sumii-Pierce-Koutavas-Wand), our method does not require induction/indices on evaluation derivation/steps (which may complicate the proofs of congruence, transitivity, and the combination with up-to techniques), or sophisticated methods such as Howe's for proving congruence. It also scales from the pure lambda-calculi to the richer calculi with simple congruence proofs.

The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in MA. We also derive some formulas that capture finitess of a term, name occurrences and persistence. We study extensions of the calculus involving more complex forms of communications, and we define characteristic formulas for the equivalence induced by the logic on a subcalculus of MA. This subcalculus is defined by imposing an image-finiteness condition on the reducts of a MA process.

A process $M$ terminates if it cannot produce an infinite sequence of reductions $M \mathop{\rightarrow}^{\tau} M_1\mathop{\rightarrow}^{\tau} M_2 \ldots$ . Termination is a useful property in concurrency. For instance, a terminating applet, when loaded on a machine, will not run for ever, possibly absorbing all computing resources (a ‘denial of service’ attack). Similarly, termination guarantees that queries to a given service originate only finite computations. We ensure termination of a non-trivial subset of the $\pi$ -calculus by a combination of conditions on types and on the syntax. The proof of termination is in two parts. The first uses the technique of logical relations – a well-know technique of $\lambda$ -calculi – on a small set of non-deterministic ‘functional’ processes. The second part of the proof uses techniques of process calculi, in particular, techniques of behavioural preorders.

This is a summary of topics that the author discussed at LICS'04. The author intends to expand substantially some of them, notably the part on the origins of bisimulation (and co-induction).

The asynchronous $\pi$ -calculus has been considered as the basis of experimental programming languages (or proposals for programming languages) like Pict, Join and TyCO. However, on closer inspection, these languages are based on an even simpler calculus, called Localised $\pi$ (L $\pi$ ), where: (a) only the output capability of names may be transmitted; (b) there is no matching or similar constructs for testing equality between names. We study the basic operational and algebraic theory of L $\pi$ . We focus on bisimulation-based behavioural equivalences, more precisely, on barbed congruence . We prove two coinductive characterisations of barbed congruence in L $\pi$ , and some basic algebraic laws. We then show applications of this theory, including: the derivability of the delayed input ; the correctness of an optimisation of the encoding of call-by-name $\lambda$ -calculus; the validity of some laws for Join; the soundness of Thielecke's axiomatic semantics of the Continuation Passing Style calculus .

We discuss some examples of the use of types for taming the behavior of concurrent systems, in particular systems of mobile processes. By "taming" we mean that we use types to enforce expected - and desirable - properties of systems. These properties would not hold without types. The examples we discuss are a printer with mobile ownership, a Boolean package implementation, and the termination property. In all these examples, the solutions based on types are only sketched. Details on the types themselves (the formal systems and their basic properties), and on the proof techniques based on types with which the equalities in the examples are proved can be found following the reference pointers, especially the work of Sangiorgi and Walker (2001) and Sangiorgi (2001). The examples are presented in the /spl pi/-calculus described by Milner (1992), a paradigmatical process calculus for message-passing concurrency.

Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences , which are similar to the interferences one finds in CCS and π-calculus; and grave interferences , which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified; the resulting calculus is called Mobile Safe Ambients (SA).The modification also has computational significance. In the MA interaction rules, an ambient may enter, exit, or open another ambient. The second ambient undergoes the action; it has no control on when the action takes place. In SA this is rectified: any movement takes place only if both participants agree.Existing type systems for MA can be easily adapted to SA. The type systems for controlling mobility, however, appear to be more powerful in SA, in that (i) type systems for MA may give more precise information when transplanted onto SA , and (ii) new type systems may be defined. Two type systems are presented that remove all grave interferences.Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. All these points are illustrated in several examples.

The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the descriptive and discriminating power of AL, focusing on the equivalence on processes induced by the logic (=/sub L/). We consider MA, and two Turing complete subsets of it, MA/sub IF/ and MA/sub IF//sup syn/, respectively defined by imposing a semantic and a syntactic constraint on process prefixes. The main contributions include: coinductive and inductive operational characterisations of =/sub L/; an axiomatisation of =/sub L/ on MA/sub IF//sup syn/; the construction of characteristic formulas for the processes in MA/sub IF/ with respect to =/sub L/; the decidability of =/sub L/ on MA/sub IF/ and on MA/sub IF//sup syn/, and its undecidability on MA.

The ambient logic has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. To understand the extensionality and the intensionality of the logic, the equivalence on MA processes induced by the logic (=L) iscompared with the standard MA behavioural equivalence and with structural congruence (an intensional equivalence, used as an auxiliary relation in thedefinition of satisfaction of the logic). The main contributions include a co-inductive characterisation of <=L as a form of labelled bisimilarity, and axiomatisations of <=L on the synchronous and asynchronous (finite) calculus. The study shows that, surprisingly, the logic allows us to observe the internal structure of the processes at a very finegrained detail, much in the same way as structural congruence does. A spin-off of the study is a better understanding of behavioural equivalence in Ambient-like calculi. For instance, behavioural equivalence is shown to be insensitive to stuttering phenomena originated by processes that may repeatedly enter and exit an ambient.

Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one finds in CCS and φ-calculus; and grave interferences, which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified. On the new calculus, the Mobile Safe Ambients (SA), a type system is defined that: controls the mobility of ambients; removes all grave interferences. Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. These points are illustrated on several examples.

We investigateparametric polymorphismin message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambda-calculus of Girard and Reynolds. Polymorphism constrains the power of observers by preventing them from directly manipulating data values whose types are abstract, leading to notions of equivalence much coarser than the standard untyped ones. We study the nature of these constraints through simple examples of concurrent abstract data types and develop basic theoretical machinery for establishing bisimilarity of polymorphic processes. We also observe some surprising interactions between polymorphism and aliasing, drawing examples from both the polymorphic pi-calculus and ML.

We study barbed equivalence in name-passing languages where there is no matching construct for testing equality between names. We concentrate on the /spl pi/-calculus with capability types and subtypes, of which the untyped /spl pi/-calculus without matching is a special case. We give a coinductive characterisation of typed barbed equivalence, and present "bisimulation up-to" techniques to enhance the resulting coinductive proof method. We then use these techniques to prove some process equalities that fail in the ordinary /spl pi/-calculus.

We investigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambda-calculus of Girard and Reynolds.Polymorphism constrains the power of observers by preventing them from directly manipulating data values whose types are abstract, leading to notions of equivalence much coarser than the standard untyped ones. We study the nature of these constraints through simple examples of concurrent abstract data types and develop basic theoretical machinery for establishing bisimilarity of polymorphic processes.We also observe some surprising interactions between polymorphism and aliasing, drawing examples from both the polymorphic pi-calculus and ML.

This paper provides both a fully abstract (domain-theoretic) model for the /spl pi/-calculus and a universal (set-theoretic) model for the finite /spl pi/-calculus with respect to strong late bisimulation and congruence. This is done by: considering categorical models, defining a metalanguage for these models, and translating the /spl pi/-calculus into the metalanguage. A technical novelty of our approach is an abstract proof of full abstraction: The result on full abstraction for the finite /spl pi/-calculus in the set-theoretic model is axiomatically extended to the whole /spl pi/-calculus with respect to the domain-theoretic interpretation. In this proof, a central role is played by the description of non-determinism as a free construction and by the equational theory of the metalanguage.

The π-calculus is a process algebra that supports mobility by focusing on the communication of channels. Milner's presentation of the π-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. We extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed λ-calculi. The greater precision of our type discipline yields stronger versions of standard theorems on the π-calculus. These can be used, for example, to obtain the validity of β-reduction for the more efficient of Milner's encodings of the call-by-value λ-calculus, which fails in the ordinary π-calculus. We define the syntax, typing, subtyping, and operational semantics of our calculus, prove that the typing rules are sound, apply the system to Milner's λ-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.

The pi -calculus is a process algebra that supports process mobility by focusing on the communication of channels. R. Milner's (1991) presentation of the pi -calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. The authors extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed lambda -calculi. The greater precision of their type discipline yields stronger versions of some standard theorems about the pi -calculus. These can be used, for example, to obtain the validity of beta -reduction for the more efficient of Milner's encodings of the call-by-value lambda -calculus, for which beta -reduction does not hold in the ordinary pi -calculus. The authors define the syntax, typing, subtyping, and operational semantics of their calculus, prove that the typing rules are sound, apply the system to Milner's lambda -calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.>

The use of lambda calculus in richer settings, possibly involving parallelism, is examined in terms of its effect on the equivalence between lambda terms, focusing on S. Abramsky's (Ph.D thesis, Univ. of London, 1987) lazy lambda calculus. First, the lambda calculus is studied within a process calculus by examining the equivalence induced by R. Milner's (1992) encoding into the pi -calculus. Exact operational and denotational characterizations for this equivalence are given. Second, Abramsky's applicative bisimulation is examined when the lambda calculus is augmented with (well-formed) operators, i.e. symbols equipped with reduction rules describing their behavior. Then, maximal discrimination is obtained when all operators are considered; it is shown that this discrimination coincides with the one given by the above equivalence and that the adoption of certain nondeterministic operators is sufficient and necessary to induce it.>