SANGIORGI , Davide

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

Coinduction is a method for specifying and reasoning about infinite data types and automata with infinite behaviour. In recent years, it has come to play an ever more important role in the theory of computing. It is studied in many disciplines, including process theory and concurrency, modal logic and automata theory. Typically, coinductive...

One of the most studied behavioural equivalences is bisimilarity, andthe main reason for its success is the associated bisimulation proofmethod, which can be further enhanced by means of `up-to bisimulation'techniques such as `up-to context'.A different proof method is discussed, based on unique solutions ofspecial forms of inequations called...

In a well-known and influential paper [17] Palamidessi has shown that the expressive power of the Asynchronous π-calculus is strictly less than that of the full (synchronous) $π$-calculus. This gap in expres-siveness has a correspondence, however, in sharper semantic properties for the former calculus, notably concerning algebraic laws. This...

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

International audience

An interpretation of Abadi and Cardelli's first-order functional {\em Object Calculus\/} \cite{AbCa94a} into a typed $\pi$-calculus is presented. The interpretation validates the subtyping relation and the typing judgements of the Object Calculus, and is computationally adequate. The type language for the $\pi$-calculus is that in \cite{PiSa93}...

This paper is concerned with the relationship between lambda-calculus and pi-calculus. The lambda-calculus talks about \emph{functions} and their\emph{applicative} behaviour. This contrasts with the pi-calculus, that talks aboutemph{processes} and their \emph{interactive} behaviour. Application is a special form of interaction, and therefore...

Up-to techniques' represent enhancements of the coinduction proof method and are widely used on coinductive behavioural relations such as bisimilarity. Abstract formulations of these coinductive techniques exist, using fixed-points or category theory. A proposal has been recently put forward for transporting the enhancements onto the concrete...

A higher-order process calculus is a calculus for communicating systems which contains higher-order constructs like communication of terms. We analyse the notion of bisimulation in these calculi. We argue that %, if static binding is assumed, both the standard definition of bisimulation (i.e., the one for CCS and related calculi), as well as...

This paper continues the study of Milner's encoding of the lazy $\lambda$-calculus into the $\pi$-calculus \cite{Mil92}. The encoding is shown to give rise to a $\lambda$-model in which, in accordance with the theory of the lazy $\lambda$-calculus, conditional extensionality holds. However, the model is not fully abstract. To obtain full...

The $\pi$-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 $\pi$-calculus has much greater expressiveness than CCS, but also a much more complex mathematical theory. The...

A few forms of bisimulation and of coinductive techniques that have been proposed for higher-order languages are discussed, beginning with the pure lambda-calculus and then moving to extensions of it, notably those with non-determinism and probabilities.

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 unique solution of special forms of inequations called...

Induction is a pervasive tool in computer science and mathematics for defining objects and reasoning on them. Coinduction is the dual of induction and as such it brings in quite different tools. Today, it is widely used in computer science, but also in other fields, including artificial intelligence, cognitive science, mathematics, modal...