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.

A short version of this paper has appeared in Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023.

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

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

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.

We present a type system to guarantee termination of π-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels. Our type system is based on Deng and Sangiorgi's level-based analysis of processes. We show that the addition of i/o-types makes it possible to typecheck processes where a form oflevel polymorphismis at work. We discuss to what extent this programming idiom can be treated by previously existing proposals. We demonstrate how our system can be extended to handle the encoding of the simply-typed λ-calculus, and discuss questions related to type inference.

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

We give an axiomatisation of strong bisimilarity on a small fragment of CCS that does not feature the sum operator. This axiomatisation is then used to derive congruence of strong bisimilarity in the finite pi-calculus in absence of sum. To our knowledge, this is the only nontrivial subcalculus of the pi-calculus that includes the full output prefix and for which strong bisimilarity is a congruence.

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.

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.

This paper discusses an application of the higher-order abstract syntax technique to general-purpose theorem proving, yielding shallow embeddings of the binders of formalized languages. Higher-order abstract syntax has been applied with success in specialized logical frameworks which satisfy a closed-world assumption. As more general environments (like Isabelle/HOL or Coq) do not support this closed-world assumption, higher-order abstract syntax may yield exotic terms, that is, datatypes may produce more terms than there should actually be in the language. The work at hand demonstrates how such exotic terms can be eliminated by means of a two-level well-formedness predicate, further preparing the ground for an implementation of structural induction in terms of rule induction, and hence providing fully-fledged syntax analysis. In order to apply and justify well-formedness predicates, the paper develops a proof technique based on a combination of instantiations and reabstractions of higher-order terms. As an application, syntactic principles like the theory of contexts (as introduced by Honsell, Miculan, and Scagnetto) are derived, and adequacy of the predicates is shown, both within a formalization of the π-calculus in Isabelle/HOL.

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.