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.
CSL Conference 2023 Conference Paper
We outline an attempt at transporting the well-known theory of enhancements for the coinduction proof method, widely used on behavioural relations such as bisimilarity, onto the realms of inductive behaviour relations, i. e. , relations defined from inductive observables, and discuss relevant literature.
TCS Journal 2022 Journal Article
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. A crucial technical ingredient in the proofs is the recently-introduced technique of unique solutions of equations, further developed in this paper. In this respect, the paper also intends to be an extended case study on the applicability and expressiveness of the technique.
CSL Conference 2022 Conference Paper
We establish a tight connection between two models of the λ-calculus, namely Milner’s encoding into the π-calculus (precisely, the Internal π-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by π and OGS. We do so for various LTSs: the standard LTS for π and a new "concurrent" LTS for OGS; an "output-prioritised" LTS for π and the standard alternating LTS for OGS. We then show that the equivalences induced on λ-terms by all these LTSs (for π and OGS) coincide. These connections allow us to transfer results and techniques between π and OGS. In particular we import up-to techniques from π onto OGS and we derive congruence and compositionality results for OGS from those of π. The study is illustrated for call-by-value; similar results hold for call-by-name.
TCS Journal 2020 Journal Article
Proving behavioural equivalences in higher-order languages is a difficult task, because interactions involve complex values, namely terms of the language. In coinductive (i. e. , bisimulation-like) techniques for these languages, a useful enhancement is the ‘up-to context’ reasoning, whereby common pieces of context in related terms are factorised out and erased. In higher-order process languages, however, such techniques are rare, as their soundness is usually delicate and difficult to establish. In this paper we adapt the technique of unique solution of equations, that implicitly captures ‘up-to context’ reasoning, to the setting of the Higher-order π-calculus. Equations are written and solved with respect to normal bisimilarity, chosen both because of its efficiency — its clauses do not require universal quantifications on terms supplied by the external observer — and because of the challenges it poses on the ‘up-to context’ reasoning and that already show up when proving its congruence properties.
I&C Journal 2020 Journal Article
The unique solution of contractions is a proof technique for (weak) bisimilarity that overcomes certain syntactic limitations of Milner's “unique solution of equations” theorem. This paper presents an overview of a comprehensive formalisation of Milner's Calculus of Communicating Systems (CCS) in the HOL theorem prover (HOL4), with a focus towards the theory of unique solutions of equations and contractions. The formalisation consists of about 24, 000 lines (1MB) of code in total. Some refinements of the “unique solution of contractions” theory itself are obtained. In particular we remove the constraints on summation, which must be guarded, by moving from contraction to rooted contraction. We prove the “unique solution of rooted contractions” theorem and show that rooted contraction is the coarsest precongruence contained in the contraction preorder.
I&C Journal 2017 Journal Article
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.
I&C Journal 2016 Journal Article
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).
I&C Journal 2011 Journal Article
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 deterministic encoding of Minsky machines, the calculus is shown to be Turing complete. Therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Furthermore, 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.
TCS Journal 2010 Journal Article
In wireless systems, the communication mechanism combines features of broadcast, synchrony, and asynchrony. We develop an operational semantics for a calculus of wireless systems. We present different Reduction Semantics and a Labelled Transition Semantics and prove correspondence results between them. Finally, we apply CWS to the modelling of the Alternating Bit Protocol, and prove a simple correctness result as an example of the kind of properties that can be formalized in this framework. A major goal of the semantics is to describe the forms of interference among the activities of processes that are peculiar of wireless systems. Such interference occurs when a location is simultaneously reached by two transmissions. The Reduction Semantics differ on how information about the active transmissions is managed. We use the calculus to describe and analyse a few properties of a version of the Alternating Bit Protocol.
I&C Journal 2006 Journal Article
A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed π-calculus processes. The systems are obtained by successive refinements of the types of the simply typed π-calculus. For all (but one of) the type systems we also present upper bounds to the number of steps well-typed processes take to terminate. The termination proofs use techniques from term rewriting systems. We show the usefulness of the type systems on some non-trivial examples: the encodings of primitive recursive functions, the protocol for encoding separate choice in terms of parallel composition, a symbol table implemented as a dynamic chain of cells.
TCS Journal 2006 Journal Article
The impact of types on the algebraic theory of the π -calculus is studied. The type system has capability types. They allow one to distinguish between the ability to read from a channel, to write to a channel, and both to read and to write. They also give rise to a natural and powerful subtyping relation. Two variants of typed bisimilarity are considered, both in their late and in their early version. For both of them, proof systems that are sound and complete on the closed finite terms are given. For one of the two variants, a complete axiomatisation for the open finite terms is also presented.
TCS Journal 2005 Journal Article
We study the encoding of λ [ ], the call-by-name λ -calculus enriched with McCarthy's amb operator, into the π -calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the λ -calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about λ [ ] that are similar to those for the encoding of pure λ -calculi. We then use these methods to derive the most important laws concerning amb. We take bisimilarity as behavioural equivalence on the π -calculus, which sheds some light on the relationship between fairness and bisimilarity.
I&C Journal 2001 Journal Article
The partition refinement algorithm is the basis for most of the tools for checking bisimulation equivalences and for computing minimal realisations of CCS-like finite state processes. In this paper, we present a partition refinement algorithm for the π-calculus, a development of CCS where channel names can be communicated. It can be used to check bisimilarity and to compute minimal realisations of finite control processes—the π-calculus counterpart of CCS finite state processes. The algorithm is developed for strong open bisimulation and can be adapted to late and early bisimulations, as well as to weak bisimulations. To arrive at the algorithm, a few laws, proof techniques, and four characterizations of open bisimulation are proved.
TCS Journal 2001 Journal Article
We compare the first- and the higher-order paradigms for the representation of mobility in process calculi. The prototypical calculus in the first-order paradigm is the π-calculus. Here, we focus on an asynchronous π-calculus (Lπ) that may be regarded as the basis of some experimental programming languages (or proposal of programming languages) like Pict, Join, Blue. We extend Lπ so to allow the communication of higher-order values, that is values that may contain processes, and show that the extension does not add expressiveness: the resulting higher-order calculus can be compiled down into Lπ. This paper is mostly a tutorial. It also contains original contributions. The main one is the full abstraction proof, which, with respect to previous proofs, is simpler and does not rely on certain non-finitary features of the languages such as infinite summation. Another contribution is the study of optimisations of the compilation, with which we are able to handle recursive types and to prove full abstraction also for strong behavioural equivalences.
TCS Journal 1999 Journal Article
In a process calculus, we say that a name x is uniformly receptive for a process P if: (1) at any time P is ready to accept an input at x, at least as long as there are processes that could send messages at x; (2) the input offer at x is functional, that is, all messages received by P at x are applied to the same continuation. In the π-calculus this discipline is employed, for instance, when modeling functions, objects, higher-order communications, or remote-procedure calls. We formulate the discipline of uniform receptiveness by means of a type system, and then we study its impact on behavioural equivalences and process reasoning. We develop some theory and proof techniques for uniform receptiveness, and illustrate their usefulness on some non-trivial examples.
I&C Journal 1998 Journal Article
An interpretation of Abadi and Cardelli's first-order functionobject calculusinto a typedπ-calculus is presented. The interpretation validates the subtyping relation and the typing judgements of the object calculus and is computationally adequate. This is the first interpretation of a typed object-oriented language into a process calculus. The study intends to offer a contribution to understanding on the one hand, the relationship betweenπ-calculus types and conventional types of programming languages and on the other hand, the usefulness of theπ-calculus as a metalanguage for the semantics of typed object-oriented languages. The type language for theπ-calculus has Pierce and Sangiorgi's I/O annotations, to separate the capabilities of reading and writing on a channel and variant types. Technical contributions of the paper are the presentation ofvariant typesfor theπ-calculus and their typing and subtyping properties, and an analysis of behavioural equivalences in aπ-calculus with variant types.
TCS Journal 1998 Journal Article
The asynchronous π-calculus is a variant of the π-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation. Their bisimulation relies on a modified transition system where, at any moment, a process can perform any input action. In this paper we propose a new notion of bisimulation for the asynchronous π-calculus, defined on top of the standard labelled transition system. We give several characterizations of this equivalence including one in terms of Honda and Tokoro's bisimulation, and one in terms of barbed equivalence. We show that this bisimulation is preserved by name substitutions, hence by input prefix. Finally, we give a complete axiomatization of the (strong) bisimulation for finite terms.
TCS Journal 1998 Journal Article
Both for interleaving and for non-interleaving semantics, several variants of a π-calculus bisimilarity can be given which differ on the requirements imposed on name instantiations. Examples are the late, early, open and ground variants. The ground variant is the simplest because it places no requirements on name instantiations. With the exception of open bisimilarities, none of the bisimilarity considered in the literature is a congruence relation on the full π-calculus language. We show that in the case of (certain forms of) causal bisimulation the late, early, open and ground variants coincide and are congruence relations in the sublanguage of the π-calculus without matching. We also show that to obtain the same results in the case of the interleaving bisimilarity, in addition to forbidding matching it is necessary to constrain the output prefix.
I&C Journal 1996 Journal Article
Ahigher-order process calculusis a calculus for communicating systems which contains higher-order constructs like communication of terms. We analyse the notion ofbisimulationin these calculi. We argue that both the standard definition of bisimulation (i. e. , the one for CCS and related calculi), as well ashigher-order bisimulation[E. Astesiano, A. Giovini, and G. Reggio, in“STACS '88, ” Lecture Notes in Computer Science, Vol. 294, pp. 207–226, Springer-Verlag, Berlin/New York, 1988; G. Boudol, in“TAPSOFT '89, ” Lecture Notes in Computer Science, Vol. 351, pp. 149–161, Springer-Verlag, Berlin/New York, 1989; B. Thomsen, Ph. D. thesis, Dept. of Computing, Imperial College, 1990] are in general unsatisfactory, because of their over-discrimination. We propose and study a new form of bisimulation for such calculi, calledcontext bisimulation, which yields a more satisfactory discriminanting power. A drawback of context bisimulation is the heavy use of universal quantification in its definition, which is hard to handle in practice. To resolve this difficulty we introducetriggered bisimulationandnormal bisimulation, and we prove that they both coincide with context bisimulation. In the proof, we exploit thefactorisation theorem: When comparing the behaviour of two processes, it allows us to “isolate” subcomponents which might give differences, so that the analysis can be concentrated on them
TCS Journal 1996 Journal Article
Process algebra semantics can be categorised into noninterleaving semantics, where parallel composition is considered a primitive operator, and interleaving semantics, where concurrency is reduced to sequentiality plus nondeterminism. The former have an appealing intuitive justification, but the latter are mathematically more tractable. This paper addresses the study of noninterleaving semantics in the framework of process algebras for mobile systems, like π-calculus [19, 17]. We focus on location bisimulation (⁈/), in our opinion one of the most convincing non-interleaving equivalences, which aims to describe the spatial dependencies on processes. We introduce ⁈/ in π-calculus following the definition for CCS given in [5]. Our main contribution is to show that in π-calculus ⁈/ can be expressed, or implemented, within the ordinary interleaving observation equivalence [16, 19] by means of a fairly simple and fully abstract encoding. Thus, we can take advantage of the easier theory of observation equivalence to reason about ⁈/. We illustrate this with a few examples, including the proof of the congruence properties of ⁈/. We show that in π-calculus ⁈/ is not a congruence, and that the full abstraction of the encoding extends to the induced congruence. The results in the paper also shed more light on the expressive power of the π-calculus.
TCS Journal 1996 Journal Article
The π-calculus is a process algebra which originates from CCS and permits a natural modelling of mobility (i. e. , dynamic reconfigurations of the process linkage) using communication of names. Previous research has shown that the π-calculus has a much greater expressiveness than CCS, but it also has a much more complex mathematical theory. The primary goal of this work is to understand the reasons for this gap. Another goal is to compare the expressiveness of name-passing calculi, i. e. , calculi like π-calculus where mobility is achieved via exchange of names, and that of agent-passing calculi, i. e. , calculi where mobility is achieved via exchange of agents. We divide the mobility mechanisms of the π-calculus into internal and external mobility mechanisms. The study of the subcalculus which only uses internal mobility, called πI, suggests that internal mobility is responsible for much of the expressiveness of the π-calculus, whereas external mobility is responsible for many of the semantic complications. A pleasant property of πI is the full symmetry between input and output constructs. Internal mobility is strongly related to agent-passing mobility. By imposing bounds on the order of the types of πI and of the Higher-Order π-calculus (Sangiorgi, 1992) we define a hierarchy of name-passing calculi based on internal mobility and one of agent-passing calculi. We show that there is an exact correspondence, in terms of expressiveness, between the two hierarchies.
MFCS Conference 1995 Conference Paper
MFCS Conference 1990 Conference Paper