On the Expressiveness and Decidability of Higher-Order Process Calculi ∗ (2009)
Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, Alan Schmitt
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...
Type Systems for Bigraphs ⋆ (2009)
Ebbe Elsborg, Thomas T. Hildebr, Davide Sangiorgi
Abstract We propose a novel and uniform approach to type systems for (process) calculi, which roughly pushes the challenge of designing type systems and proving properties about them to the...
Nicola Mezzetti, Davide Sangiorgi
Abstract 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...
Denis Diderot, Spécialité Informatique, Mm. Pierre-louis, Curien Président, ...
pour l’obtention du Diplôme de
Logical Bisimulations and Functional Languages ⋆ (2008)
Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
Abstract. Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation...
Separability in the Ambient Logic (2008)
Hirschkoff, Daniel, Lozes, Etienne, Sangiorgi, Davide
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...
An efficient abstract machine for Safe Ambients (2008)
École Normale, Supérieure Lyon, Daniel Hirschkoff, Damien Pous, Davide Sangiorgi, École Normale, ...
Safe Ambients (SA) are a variant of the Ambient Calculus (AC) in which types can be used to avoid certain forms of interferences among processes called grave interferences. An abstract machine,...
A Distributed Abstract Machine for Safe (2008)
Davide Sangiorgi, Andrea Valente
The Ambient calculus [4] is a model for mobile distributed computing. An ambient is the unit of movement. Processes within the same ambient may exchange messages; ambients may be nested, so to form a...
Logical Bisimulations and functional languages ⋆ (2008)
Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
Abstract. Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation...
From π-calculus to Higher-Order π-calculus - and back (2007)
To Higher-order, Davide Sangiorgi
. We compare the first-order and the higher-order paradigms for the representation of mobility in process algebras. The prototypical calculus in the first-order paradigm is the ß-calculus. By...
Asynchronous process calculi: the rst-order and higher-order paradigms (Tutorial) (2007)
We compare the rst-order and the higher-order paradigms for the representation of mobility in process calculi. The prototypical calculus in the rst-order paradigm is the-calculus. Here, we focus on...
Roberto M. Amadio, Ilaria Castellani, Davide Sangiorgi
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...
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...
Environmental bisimulations for higher-order languages (2007)
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...
Environmental bisimulations for higher-order languages (2007)
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...
On the Expressiveness of the Ambient Logic (2005)
Hirschkoff, Daniel, Lozes, Etienne, Sangiorgi, Davide
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...
On the Expressiveness of the Ambient Logic (2005)
Hirschkoff, Daniel, Lozes, Etienne, Sangiorgi, Davide
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...
On the Expressiveness of the Ambient Logic (2005)
Hirschkoff, Daniel, Lozes, Etienne, Sangiorgi, Davide
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...
On the Expressiveness of the Ambient Logic (2005)
Hirschkoff, Daniel, Lozes, Etienne, Sangiorgi, Davide
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...
On the Expressiveness of the Ambient Logic (2005)
Hirschkoff, Daniel, Lozes, Etienne, Sangiorgi, Davide
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...
An efficient abstract machine for Safe Ambients. (2004)
Hirschkoff, Daniel, Pous, Damien, Sangiorgi, Davide
(eng) Safe Ambients (SA) are a variant of the Ambient Calculus (AC) in which types can be used to avoid certain forms of interferences among processes called
An Efficient Abstract Machine for Safe Ambients (2004)
Daniel Hirschkoff, Damien Pous, Davide Sangiorgi
Abstract. We describe an abstract machine, called GcPan, for the distributed execution of Safe Ambients (SA), a variant of the Ambient Calculus (AC). Our machine improves over previous proposals for...
An Efficient Abstract Machine for Safe Ambients (2004)
Daniel Hirschkoff, Damien Pous, Davide Sangiorgi
Introduction Ambients-based calculi have been proposed as models for distributed and mobile computing based onthe notion of location, called ambient. Terms in these calculi describe configurations of...
On the representation of McCarthy’s ambin the π-calculus (2004)
Arnaud Carayol, Daniel Hirschkoff, Davide Sangiorgi
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...
Towards an Algebraic Theory of Typed Mobile Processes (2004)
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...
Ensuring Termination by Typability (2004)
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...
Towards an Algebraic Theory of Typed Mobile Processes (2004)
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...
Ensuring Termination by Typability (2004)
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...
Ensuring termination by typability (2004)
Abstract. 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...
Towards an algebraic theory of typed mobile processes (2004)
Abstract. 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...
Ensuring termination by typability (2004)
Abstract 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...
On Asynchrony in Name-Passing Calculi (2002)
Massimo Merro, Davide Sangiorgi
The asynchronous #-calculus is considered the basis of experimental programming languages (or proposal of programming languages) like Pict, Join, and TyCO. However, at a closer inspection, these...
Termination of processes (2001)
Davide Sangiorgi, Josva Kleist, Josva Kleist
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS Report Series publications. Copies may be...
A distributed abstract machine for safe ambients (2001)
Davide Sangiorgi, Andrea Valente
An abstract machine for a distributed implementation of an ambient calculus is presented, and proved operationally correct. The abstract machine is dioeerent from, and simpler than, previous...
Termination of processes (2001)
calculi: languages fo r describing p ro cesses that put pa rticula r emphasis on their structure (ie, ho w p ro cesses a re constructed and the meaning of these constructions) Their semantics *...
Controlling interference in ambients (2000)
Francesca Levi, Davide Sangiorgi
Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one nds in CCS and -calculus; and grave...
Extensionality and Intensionality of the Ambient Logics (2000)
The ambient logics has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semi-structured data. To understand...
Controlling Interference in Ambients (2000)
Francesca Levi, Davide Sangiorgi
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 pi-calculus; and grave...
Behavioral equivalence in the polymorphic pi-calculus (2000)
Benjamin C. Pierce, Davide Sangiorgi
Weinvestigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in atyped process calculus analogous to the polymorphic lambdacalculus of Girard and...
Behavioral Equivalence in the Polymorphic Pi-Calculus (1999)
Pierce, Benjamin C, Sangiorgi, Davide
We investigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic λ- calculus of Girard and...
A π-calculus process semantics of concurrent idealised ALGOL (1999)
Christine Röckl, Davide Sangiorgi
We study the use of the π-calculus for semantical descriptions of languages such as Concurrent Idealised ALGOL (CIA), combining imperative, functional and concurrent features. We first present an...
Davide Sangiorgi, Inria-sophia Antipolis
Cliff Jones [Jon93a] has raised the challenge of how to prove the validity of a certain transformation that increases the concurrent activity in a system of concurrent objects. We present a proof of...
Behavioral Equivalence in the Polymorphic Pi-Calculus (1999)
Benjamin C. Pierce, Davide Sangiorgi
We investigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambdacalculus of Girard...
Interpreting functions as π-calculus processes: a tutorial (1999)
This paper is concerned with the relationship between-calculus and ��-calculus. The-calculus talks about functions and their applicative behaviour. This contrasts with the ��-calculus, that...
Typed Pi-Calculus At Work: A Proof of... (1999)
this paper we show a proof of correctness of the hardest of Jones's concrete transformations, for which we exploit a typed ß-calculus.
Interpreting Functions as pi-calculus Processes: a Tutorial (1998)
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...
Interpreting Functions as pi-calculus Processes: a Tutorial (1998)
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...
Interpreting Functions as pi-calculus Processes: a Tutorial (1998)
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...
Surrogates in jeblik: Towards Migration in Obliq (1998)
Hans Huttel, Josva Kleist, Uwe Nestmann, Davide Sangiorgi
In Cardelli's lexically scoped, distributed, object-based programming language Obliq, object migration was suggested as creating a (remote) copy of an objects' state at the target site,...
Some Congruence Properties for π-calculus Bisimilarities (1998)
Michele Boreale, Davide Sangiorgi, Implies Q
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...
Some Congruence Properties for π-calculus Bisimilarities (1998)
Michele Boreale, Davide Sangiorgi, Implies Q
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...
On Asynchrony in Name-Passing Calculi (1998)
Massimo Merro, Davide Sangiorgi
The asynchronous pi-calculus is considered the basis of experimental programming languages (or proposal of programming languages) like Pict, Join, and Blue calculus. However, at a closer inspection,...
This document in subdirectoryRS/98/52/ Imperative Objects and Mobile Processes (1998)
Josva Kleist, Davide Sangiorgi, Josva Kleist, Davide Sangiorgi
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
The name discipline of uniform receptiveness (Extended Abstract) (1997)
this paper, we study the situation in which certain names are uniformly receptive. A name x is receptive in a process P if at any time P is able of offering an input at x (at least as long as there...
The Name Discipline of Uniform Receptiveness (1997)
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...
Behavioral Equivalence in the Polymorphic Pi-Calculus (1997)
Benjamin Pierce Computer, Benjamin C. Pierce, Davide Sangiorgi
We investigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambdacalculus of Girard...
Imperative Objects and Mobile Processes (1997)
Josva Kleist, Davide Sangiorgi
An interpretation of Abadi and Cardelli's first-order Imperative Object Calculus into a typed -calculus is presented. The interpretation validates the subtyping relation and the typing...
Behavioral Equivalence in the Polymorphic Pi-Calculus (1997)
Benjamin C. Pierce, Benjamin C. Pierce, Davide Sangiorgi, Davide Sangiorgi, Projet Meije
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...
Imperative Objects and Mobile Processes DRAFT (1997)
Josva Kleist, Davide Sangiorgi
An interpretation of Abadi and Cardelli’s first-order Imperative Object Calculus into a typed π-calculus is presented. The interpretation validates the subtyping relation and the typing judgements...
An Interpretation of Typed Objects Into Typed $\pi$-calculus (1996)
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...
On Bisimulations for the Asynchronous pi-calculus (1996)
Amadio, Roberto M., Castellani, Ilaria, Sangiorgi, Davide
The {\em asynchronous $\pi$-calculus\/} is a variant of the $\pi$-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation....
Some Congruence Properties for pi-calculus Bisimilarities (1996)
Boreale, Michele, Sangiorgi, Davide
Both for interleaving and for non-interleaving semantics, several variants of a $\pi$-calculus bisimilarity can be given which differ on the requirements imposed on name instantiations. Examples are...
An Interpretation of Typed Objects Into Typed $\pi$-calculus (1996)
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...
On Bisimulations for the Asynchronous pi-calculus (1996)
Amadio, Roberto M., Castellani, Ilaria, Sangiorgi, Davide
The {\em asynchronous $\pi$-calculus\/} is a variant of the $\pi$-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation....
Some Congruence Properties for pi-calculus Bisimilarities (1996)
Boreale, Michele, Sangiorgi, Davide
Both for interleaving and for non-interleaving semantics, several variants of a $\pi$-calculus bisimilarity can be given which differ on the requirements imposed on name instantiations. Examples are...
An Interpretation of Typed Objects Into Typed $\pi$-calculus (1996)
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...
On Bisimulations for the Asynchronous pi-calculus (1996)
Amadio, Roberto M., Castellani, Ilaria, Sangiorgi, Davide
The {\em asynchronous $\pi$-calculus\/} is a variant of the $\pi$-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation....
Some Congruence Properties for pi-calculus Bisimilarities (1996)
Boreale, Michele, Sangiorgi, Davide
Both for interleaving and for non-interleaving semantics, several variants of a $\pi$-calculus bisimilarity can be given which differ on the requirements imposed on name instantiations. Examples are...
Typing and subtyping for mobile processes (1996)
Benjamin Pierce, Davide Sangiorgi
The-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the-calculus includes a type system assigning arities to...
Typing and subtyping for mobile processes (1996)
Benjamin Pierce, Davide Sangiorgi
The-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the-calculus includes a type system assigning arities to...
An interpretation of Typed Objects into Typed π-calculus (1996)
Davide Sangiorgi, Davide Sangiorgi, Projet Meije
An interpretation of Abadi and Cardelli's first-order functional Object Calculus [AC94b] into a typed -calculus is presented. The interpretation validates the subtyping relation and the typing...
Bisimulation for Higher-Order Process Calculi (1996)
N Rr, Davide Sangiorgi, Davide Sangiorgi
: 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....
Some Congruence Properties for π-calculus Bisimilarities (1996)
Michele Boreale, Michele Boreale, Davide Sangiorgi, Davide Sangiorgi, Projet Meije
Both for interleaving and for non-interleaving semantics, several variants of a pi-calculus bisimilarity can be given which differ on the requirements imposed on name instantiations. Examples are the...
Bisimulation for Higher-Order Process Calculi (1996)
Davide Sangiorgi, Inria Sophia Antipolis
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...
On Bisimulations for the Asynchronous π-Calculus (1996)
Roberto M. Amadio, Roberto M. Amadio, Ilaria Castellani, Ilaria Castellani, Davide Sangiorgi, Davide Sangiorgi, ...
The asynchronous pi-calculus is a variant of the pi-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation. Their...
Behavioral Equivalence in the Polymorphic Pi-Calculus (1996)
Benjamin C. Pierce, Davide Sangiorgi
We investigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambdacalculus of Girard...
Typing and Subtyping for Mobile Processes (1996)
Benjamin Pierce, Davide Sangiorgi
The ß-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the ß-calculus includes a type system assigning...
Typing and Subtyping for Mobile Processes (1996)
Benjamin Pierce, Davide Sangiorgi
The pi-calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the pi-calculus includes a type system assigning...
A Partition Refinement Algorithm for the pi-calculus (1996)
Marco Pistore, Davide Sangiorgi
. The partition refinement algorithm [10, 6] is the basis for most of the tools for checking bisimulation equivalences and for computing minimal realisations of CCS-like finite state processes. In...
Bisimulation for higher-order process calculi (1995)
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...
Lazy functions and mobile processes (1995)
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...
pi-calculus, internal mobility, and agent-passing calculi (1995)
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....
Bisimulation for higher-order process calculi (1995)
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...
Lazy functions and mobile processes (1995)
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...
pi-calculus, internal mobility, and agent-passing calculi (1995)
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....
Bisimulation for higher-order process calculi (1995)
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...
Lazy functions and mobile processes (1995)
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...
pi-calculus, internal mobility, and agent-passing calculi (1995)
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....
Lazy Functions and Mobile Processes (1995)
Calcul Symbolique, Davide Sangiorgi, Davide Sangiorgi, Projet Meije
: This paper continues the study of Milner's encoding of the lazy -calculus into the ß-calculus [Mil90]. The encoding is shown to give rise to a -model in which, in accordance with the theory...
A Fully Abstract Semantics for Causality in the Pi-Calculus (1995)
Michele Boreale, Davide Sangiorgi
We examine the meaning of causality in calculi for mobile processes like the ß-calculus, and we investigate the relationship between interleaving and causal semantics for such calculi. We separate...
π-Calculus, Internal Mobility, and Agent-Passing Calculi (1995)
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...
π-Calculus, Internal Mobility, and Agent-Passing Calculi (1995)
Calcul Symbolique, Davide Sangiorgi, Davide Sangiorgi
: 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....
On the Bisimulation Proof Method (1994)
Davide Sangiorgi, Antipolis Cedex
The most popular method for establishing bisimilarities among processes is to exhibit bisimulation relations. By definition, R is a bisimulation relation if R progresses to R itself, i.e., pairs of...
The Lazy Lambda Calculus in a Concurrency Scenario (Extended Abstract) (1994)
) Davide Sangiorgi LFCS - Department of Computer Science Edinburgh University Edinburgh - EH9 3JZ - UK Abstract The use of lambda calculus in richer settings, possibly involving parallelism, is...
The Lazy Lambda Calculus in a Concurrency Scenario (1994)
The use of -calculus in richer settings, possibly involving parallelism, is examined in terms of the effect on the equivalence between -terms. We concentrate on Abramsky's lazy -calculus...
On the Bisimulation Proof Method (1994)
Davide Sangiorgi, Inria Sophia Antipolis, Antipolis Cedex
The most popular method for establishing bisimilarities among processes is to exhibit bisimulation relations. By definition, R is a bisimulation relation if R progresses to R itself, i.e., pairs of...
Locality and Non-interleaving Semantics in calculi for mobile processes (1994)
Process algebra semantics can be categorised into non-interleaving semantics, where parallel composition is considered a primitive operator, and interleaving semantics, where concurrency is reduced...
Algebraic Theories for Name-Passing Calculi (1994)
Joachim Parrow, Davide Sangiorgi
In a theory of processes the names are atomic data items which can be exchanged and tested for identity. A well-known example of a calculus for name-passing is the ß-calculus, where names...
"Also published as ECS-LFCS-93-266"--Cover.
Algebraic theories for name-passing calculi (1993)
Parrow, Joachim, Sangiorgi, Davide
In a theory of processes the names are atomic data which can be exchanged and tested for identity, but which admit no other functions or predicates. A well-known example of a calculus for...
Algebraic Theories for Name-Passing Calculi (1993)
Davide Sangiorgi, Joachim Parrow, Joachim Parrow
In a theory of processes the names are atomic data items which can be exchanged and tested for identity. A well-known example of a calculus for name-passing is the ß-calculus, where names...
Locality and True-concurrency in calculi for mobile processes (1993)
. Process algebra semantics can be categorised into true-concurrency semantics, where parallel composition is considered a primitive operator, and interleaving semantics, where concurrency is reduced...
An investigation into Functions as Processes (1993)
. In [Mil90] Milner examines the encoding of the -calculus into the ß-calculus [MPW92]. The former is the universally accepted basis for computations with functions, the latter aims at being its...
A Theory of Bisimulation for the pi-calculus (1993)
We study a new formulation of bisimulation for the -calculus [MPW92], which we have called open bisimulation ( ). In contrast with the previously known bisimilarity equivalences, is preserved by all...
Typing and Subtyping for Mobile Processes (Extended Abstract) (1992)
Benjamin Pierce, Davide Sangiorgi
The -calculus is a process algebra that supports process mobility by focusing on the communication of channels. Milner's presentation of the -calculus includes a type system assigning arities to...
Robin Milner, Davide Sangiorgi, Edinburgh Eh Jz
Machine [8]. In this technique, axioms for a structural congruence relation are introduced prior to the reduction system, in order to to break a rigid, geometrical vision of concurrency; then...
Static and dynamic typing for the termination of mobile processes (1970)
Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi
A process terminates if all its reduction sequences are finite. We propose two type systems that ensure termination of ð -calculus processes. Our first type system is purely static. It refines...