Author name cluster

D. Sangiorgi

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.

4 papers

1 author row

I&C Journal 2002 Journal Article

A Fully Abstract Model for the π-calculus

M.P. Fiore
E. Moggi
D. Sangiorgi

This paper provides both a fully abstract (domain-theoretic) model for the π-calculus and a universal (set-theoretic) model for the finite π-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 π-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 π-calculus in the set-theoretic model is axiomatically extended to the whole π-calculus with respect to the domain-theoretic interpretation. In this proof, a central role is played by the description of nondeterminism as a free construction and by the equational theory of the metalanguage.

Details DOI

I&C Journal 1995 Journal Article

Algebraic Theories for Name-Passing Calculi

J. Parrow
D. Sangiorgi

In a theory of processes the names are atomic data items which can be exchanged and tested for identify. A well-known example of a calculus for name-passing is the π-calculus, where names are additionally used as communication ports. We provide complete axiomatisations of late and early bisimulation equivalences in such calculi. Since neither of the equivalences is a congruence we also axiomatise the corresponding largest congruences. We consider a few variations of the signature of the language; among these, a calculus of deterministic processes which is reminiscent of sequential functional programs with a conditional construct. Most of our axioms are shown to be independent. The axiom systems differ only by a few simple axioms and reveal the similarities and the symmetries of the calculi and the equivalences.

Details DOI

I&C Journal 1994 Journal Article

The Lazy Lambda Calculus in a Concurrency Scenario

D. Sangiorgi

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 and we follow two directions. Firstly, the λ-calculus is studied within a process calculus by examining the equivalence [formula] induced by Milner′s encoding into the π-calculus. We start from a characterization of [formula] presented in (Sangiorgi D. , 1992) Ph. D. thesis. We derive a few simpler operational characterisations, from which we prove full abstraction w. r. t. Levy-Longo Trees. Secondly, we examine Abramsky′s applicative bisimulation when the λ-calculus is augmented with (well-formed) operators, that is symbols equipped with reduction rules describing their behaviour. In this way, the maximal discrimination between pure λ-terms (i. e. , the finest behavioural equivalence) is obtained when all operators are used. We prove that the presence of certain non-deterministic operators is sufficient and necessary to induce it and that it coincides with the discrimination given by [formula]. We conclude that the introduction of non-determinism into the λ-calculus is exactly what makes applicative bisimulation appropriate for reasoning about the functional terms when concurrent features are also present in the language, or when they are embedded into a concurrent language.

Details DOI

TCS Journal 1991 Journal Article

Nonacceptability criteria and closure properties for the class of languages accepted by binary systolic tree automata

E. Fachini
A. Maggiolo Schettini
G. Resta
D. Sangiorgi

In this paper a contribution is given to the solution of the problem of finding an inductive characterization of the class of languages accepted by binary systolic tree automata, L (BSTA), in terms of the closure of a class of languages with respect to certain operations. It is shown that L (BSTA) is closed with respect to some new operations: selective concatenation, restricted concatenation and restricted iteration. The known nonclosure of L (BSTA) with respect to classical language operations, like concatenation and Kleene iteration is proved here by using a new nonacceptability criterion.

Details DOI