Chapter 3: Management
3.1 Consortium level
The main management of the project is done at INRIA, Rocquencourt, and
at ICL.
The following activities at the consortium level have taken place
during the third year of the CONFER2 working group:
Two workshops have been held. The first took place in April 1999 in
Pisa with 20 presentations and 30 participants, and was organized by
Gianluigi Ferrari and Ugo Montanari. The second workshop took place in
November 1999 at University of Paris 7 (in the new buildings of rue du
Chevaleret) near ENS in Paris with 14 presentations and 30
participants. It was organized by PierreLouis Curien.
As specified in §2.6 of the Working Group Programme, the vast
majority of the activity of CONFER2 is devoted to the organization of
2 workshops per year. The cost statement forms will strengthen this
distribution of the activity, although some of the funds are still
reserved for travel expenses between sites.
Finally, we obtained in 1999 the permission for a oneyear
prolongation of Confer2 without total budget change.
3.2 Università di Bologna
3.2.1 Research
The research activity in Bologna, organized along the main
task of the Working Group, has been the following:
 Calculi

In this area, we have been involved in the
analysis of bisimulation in the framework of joincalculus, in the
expressivity of the fusioncalculus and the study
of a novel classbased concurrent calculus  the objective
joincalculus.
Analysis of Bisimulation
We have finished the full paper about the theory of bisimulation
in the joincalculus [FL99] (the extended abstract was published in
the Procomet conference in 1998).
To this purpose, we have proved that several formulations of
bisimulation actually yield the same equivalence and that bisimulation
and barbed congruence coincide in the presence
of nametesting.
Expressivity of the Fusion Calculus In [LV99] we
present a calculus of mobile processes without prefix and summation,
and using two different encodings we show that it can express both
action prefix and guarded summation. One encoding gives a strong
correspondence but uses a match operator; the other yields a slightly
weaker correspondence but uses no additional operators.
The composition of concurrent classes In [FLMR99] we
present an elementary classbased calculus of concurrent objects
obtained from the joincalculus by introducing primitive record
structure. We provide inheritance as the combination of a few
operators to assemble objects from partial joincalculus definitions.
As usual, method definitions and private fields of a parent class can
be reused, overridden, or extended. As expected with concurrent
objects, inheritance admits some but not all refinements of the
synchronization patterns of the parent class.
 Programming Languages
 We have published the book ``Optimal
Implementation of Functional Programming Languages'' [AG98], where most
of our previous results about optimal implementations have been collected.
3.2.2 Workshops, Travels and Visits
No travel and visit.
3.2.3 Publications

[AG98]
 A. Asperti, S.Guerrini The
Optimal Implementation of Functional Programming Languages.
in ``Cambridge Tracts in Theoretical Computer
Science'' Series, Cambridge University Press, December 1998.
 [FL99]
 C. Fournet, C. Laneve: Bisimulations in the JoinCalculus. Submitted to a Journal. June 1999.
 [FLMR99]
 C. Fournet, C. Laneve, L. Maranget, D. Rèmy: Assembling Objects with Internal Concurrency. Draft, October 1999.
 [LV99]
 C. Laneve, B. Victor:
Solos in Concert. ICALP'99, LNCS 1644.
3.3 University of Cambridge
3.3.1 University of Cambridge
3.3.1.1 Research directions
Categorical models of process calculi
Cattani received his PhD from Aarhus University (DK) in
May [CaPhD99].
Progressing from his thesis work, together with Fiore from Sussex and
Winskel from Aarhus, he has recently introduced a systematic
treatment of weak bisimulation and observational congruence on
presheaf models [FCW99]. This work was
also presented at the CONFER2 Workshop in Pisa.
The paper [PCW99], submitted last year and
mentioned in the Periodic Progress Report of 1998, has
now been accepted for publication.
Together with Sewell he is presently developing models for
mobileprocess calculi, e.g., the pcalculus, which extend
traditional ones such as (asynchronous) transition systems and
synchronization trees, by having indexed sets of states to account for
the dynamic generation and communication of channel names.
Bisimulation and Action Calculi
Leifer is investigating general methods for deriving labeled transition
systems from reduction rules in such a way that bisimulation over the
derived labeled transitions is a congruence. The setting for this
work is Milner's action calculi. Over this past year, Leifer has
strengthened his results to operate on action calculi rich enough to
include the synchronous picalculus; in this case the derived
bisimulation corresponds with early bisimulation, a wellknown
equivalence for pi.
His work relies on properties of context factorization in action
calculi. He is constructing a category with terms as objects and
contexts as morphisms to investigate the universal properties of the
factorizations.
The work of Sewell on the problem in settings without name binding has been
accepted for publication
[Sew99a].
Gardner has recently shown the precise link between the synchronous
pcalculus and the action calculus for the pcalculus,
strengthening previous results.
Gardner is supervising the design and construction of a specification
tool for action graphs, together with Michael Norrish, which allows
the user to naturally move between the syntactic and graphical
presentations. They have solved a difficult matching problem to
identify instances of redexes in a graph, and with Andrei Serjantov
have extended the tool to the reflexive case.
Fusions, Naming and Graphs Wischik and Gardner have
developed a pcalculus with fusions, called the p_{F}calculus,
which arose from their work on process frameworks described below. It
turns out that the p_{F}calculus is related to the fusion calculus
of Parrow and Victor, although the naming primitives are different,
and to work by Honda and by Merro on equators in the pcalculus.
They have identified bisimulation congruences for the
p_{F}calculus. There are simple embeddings of the the
pcalculus, the p_{I}calculus and the fusion calculus in the
p_{F}calculus. They are currently showing that bisimulation
congruences for these calculi are related to bisimulation congruences
for their embeddings in the p_{F}calculus.
Wischik and Gardner are further exploring the role of naming
constructs in graphical frameworks. In particular, they have
introduced a process framework based on the same naming primitives as
the p_{F}calculus. This framework conservatively extends the
reflexive action calculus framework. It seems to give a more direct
presentation of many examples, and has a simple general notion of
barbed congruence. Their aim is to show that the barbed congruence for
the framework corresponds to natural notions of congruence in specific
examples.
Nomadic Pict
Sewell, Unyapoth and Wojciechowski have continued work on the
Nomadic Pict distributed programming language, studying
the design, semantic definition and implementation of
locationindependent communication primitives for mobile agents.
The language implementation (by Wojciechowski) has now been completed;
it is being used to experiment with infrastructure algorithms.
The language and example infrastructures have been described in
[SWP99b]
(with Pierce) and in
[WS99].
On the semantic side, Unyapoth has developed the theory of the
Nomadic pcalculus to support infrastructure correctness
proofs. The calculus has been equipped with operational semantics
(both labeled transition and reduction), a type system and notions of
bisimulation; work on partial confluence proof techniques is ongoing.
Secure Encapsulation Sewell and Vitek (of Purdue
University) are considering the problem of assembling concurrent
software systems from untrusted or partially trusted offtheshelf
components, using wrapper programs to encapsulate components
and enforce security policies. In [SV99a, SV99b] they introduced
the boxp process calculus with constrained interaction to
express wrappers and discussed the rigorous formulation of their
security properties. In [SV99c] they address the verification of
wrapper information flow properties, presenting a novel causal
type system that statically captures the allowed flows between
wrapped possiblybadlytyped components; it is used to prove that a
unidirectionalflow wrapper enforces a causal flow property.
Polynomial Pi Sawle and Milner have developed the
Polynomial Pi Calculus, an extension of the pcalculus with
multiple synchronization. An animation tool has been implemented;
work on applying it to verifying properties of security protocols is
underway.
3.3.1.2 Persons and Exchanges
Leifer visited INRIA Rocquencourt for a week in April and a month in
May/June 1999. Gardner visited Amsterdam for two weeks, INRIA
Rocquencourt for a week and Sussex. Cattani, Gardner, Leifer, Sewell
and Wischik attended the CONFER workshop in Pisa.
3.3.2 Publications

[CaPhD99]

G. L. Cattani.
Presheaf Models for Concurrency.
PhD Thesis, University of Aarhus, 1999.
 [FCW99]

M. Fiore, G. L. Cattani and G. Winskel.
Weak Bisimulation and Open Maps.
In Proceedings of the 14th Symposium on Logic in
Computer Science, LICS '99, pages 6776, IEEE Press,
1999.
 [PCW99]

A. J. Power, G. L. Cattani and G. Winskel.
A Representation Result for Free Cocompletions.
To appear in Journal of Pure
and Applied Algebra, 1999.
 [Ga99a]

Philippa Gardner.
Closed Action Calculi.
Journal of Theoretical Computer Science, 1999. To appear.
 [GW99]

Philippa Gardner and Lucian Wischik.
Symmetric Action Calculi.
Extended abstract, Express 99.
 [Ga99b]

Philippa Gardner.
Interaction Nets, Sharing graphs and Action Calculi.
Submission in
association with the Mathfit Workshop on Process Algebra, January 99.
 [SV99a]

Peter Sewell and Jan Vitek.
Secure composition of insecure components.
Technical Report 463, Computer Laboratory, University of Cambridge,
April 1999.
 [SV99b]

Peter Sewell and Jan Vitek.
Secure composition of insecure components.
In Proceedings of the 12th IEEE Computer Security Foundations
Workshop. Mordano, Italy, pages 136150. IEEE Computer Society, June 1999.
 [SV99c]

Peter Sewell and Jan Vitek.
Secure Composition of Untrusted Code:
Wrappers and Causality Types.
Submitted for publication.
 [Sew99a]

Peter Sewell.
From rewrite rules to bisimulation congruences.
Theoretical Computer Science, 1999.
Invited submission, to appear in a special issue for CONCUR 98.
 [SWP99b]

Peter Sewell, Pawe T. Wojciechowski, and Benjamin C. Pierce.
Locationindependent communication for mobile agents: a twolevel
architecture.
In Internet Programming Languages, LNCS 1686. SpringerVerlag, 1999.
 [WS99]

Pawe T. Wojciechowski and Peter Sewell.
Nomadic Pict: Language and infrastructure design for mobile
agents.
In Proceedings of ASA/MA 99: Agent Systems and
Applications/Mobile Agents, IEEE, October 1999.
 [Sew99pi]

Peter Sewell.
A brief introduction to applied p, January 1999.
Lecture notes for the Mathfit Instructional Meeting on Recent
Advances in Semantics and Types for Concurrency: Theory and Practice, July
1998.
3.4 CWI
3.4.1 Research Directions
J.W. Klop has completed work on origin tracking in lambda calculus and
term rewriting. This work is reported in the paper
``Descendants and Origins in term Rewriting'',
accepted for publication in Information and Computation,
also to be found at http://www.cs.vu.nl/ rdv/dotr.ps.gz
(Joint work with I. Bethke and R.C. de Vrijer)
J.W. Klop (together with I. Bethke and R.C. de Vrijer)
has completed a study on extensions of partial
combinatory algebras, published in
Math. Struct. in Comp.Science (1999) vol.9, pp.483505.
(Also at ftp://ftp.cs.vu.nl/pub/papers/theory/IR448.ps.Z)
J.W. Klop, V. van Oostrom and R.C. de Vrijer have completed a
study of infinite reduction diagrams, yielding an
alternative proof of the theorem of De Bruijn and
van Oostrom concerning confluence by decreasing
diagrams: 'A geometric proof of confluence by
decreasing diagrams.'
To be published in special issue of JLC.
(Also at ftp://ftp.cs.vu.nl/pub/papers/theory/IR448.ps.Z)
3.4.2 Workshops, Travels and Visits
J.W. Klop attended the CONFER2 Workshop in Pisa, March, 1999.
J.W. Klop, F. van Raamsdonk, V. van Oostrom
attended the Workshop Terms and Types, April 1013,
HeriotWatt, Edinburgh.
J.W. Klop gave an invited tutorial 'Ten topics in Term Rewriting'
at the Logic Colloquium '99, Utrecht, The Netherlands, August 16, 1999.
3.5 University of Edinburgh
3.6 ENS
3.6.1 Research Directions
Work at the ENS site has gone into four directions.

Probabilistic games: Vincent Danos and Russel Harmer, a
former student of Pasquale Malacaria, are working on an extension of
games semantics to model functional or imperative computations
extended with a random instruction.
So far, they have proved that in their setting of probabilistic
strategies, the coin strategy that returns true or false with equal
chances, is universal, that is any probabilistic strategy can be
factorized as a deterministic one composed with the coin.
 Games semantics and denotational semantics: In collaboration
with Samson Abramsky, PaulAndré Melliès has introduced in
[AbMe99] a concurrent game model of linear logic and proved a
full completeness result for multiplicative additive linear logic.
Then, by polarizing the concurrent game model, PaulAndré Melliès
has unveiled the dynamical content of the hypercoherence space model
introduced by Thomas Ehrhard in 1993. The idea is to construct a full functor U from the game model G to the hypercoherence
model H, and to show that U respects the constructions of
linear logic; the ``fullness'' of U asserts that every static
function (or clique) of H may be implemented as a dynamical and concurrent strategy [Me99a].
Another important question, already attacked by Thomas Ehrhard in his
work on the extensional collapse of sequential algorithms, and by
Patrick Baillot, Vincent Danos, Thomas Ehrhard and Laurent Regnier in
their work on timeless games [Da99], is the connection between a
static model like, say hypercoherence spaces, and sequential
game models. After [BDER98], one is tempted to see the problem
as purely gametheoretical, of understanding the connection between
the sequential and the concurrent version of game semantics. This
approach is currently under investigation.
 Callbyname, callbyvalue, continuations and sequent calculus:
About four years ago, Vincent Danos, JeanBaptiste Joinet and
Harold Schellinx, have packed a comprehensive study of sequent
calculi for classical logic, most notably LKT, LKQ and LKTQ, that
one could embed in linear logic. In [Da99] a sound and intuitive
continuation calculus is attached to LKQ, yielding a `CurryHoward'
configuration. Plugging in a standard embedding of natural deduction
in sequent calculus, one retrieves a Plotkinlike continuation
passing style
compilation of callbyvalue lambdacalculus with control. In
collaboration with a student, Charles Harris,
Vincent Danos is now trying to set up a mixed
callbyvalue/callbyname CPS compilation starting from LKTQ.
On the other hand, PierreLouis Curien and Hugo Herbelin have just
started to work independently along similar lines: they have
proposed a syntax for callbyvalue calculi that is directly
inspired by the sequent calculus LKQ.
This syntax offers an attractive logical explanation of the atomic
steps of the callbyvalue abstract machines, and enhances
symmetries and dualities (callbyname / callbyvalue, input /
output)
 Axiomatic rewriting: PaulAndré Melliès has entirely
rewritten the
second part of his four articles on axiomatic rewriting theory.
The paper [Me99b] contains a short and elegant
proof of needed normalization for lambdasigmaterms.
The argument is based on the following observation:
that a standard rewriting path M® N
in the lscalculus projects
as a standard rewriting path s(M)® N
when N is a lterm.
3.6.2 Publications

[Da99]

V. Danos.(1999)
Sequent Calculus and Continuation Passing Style Compilation.
To appear in the Proceedings of the 11th Congress of Logic,
Methodology and Philosophy of
Science, held in Cracow, Kluwer.
 [AbMe99]

S. Abramsky, P.A. Melliès.(1999)
Concurrent games and full completeness.
Proceedings of LiCS'99, Trento.
 [Me99a]

P.A. Melliès.(1999)
Hypercoherence spaces as concurrent games,
in preparation.
 [Me99b]

P.A. Melliès.(1999)
Axiomatic rewriting theory II:
The lambdasigma calculus enjoys finite normalization cones.
Submitted.
 [BDER98]

P. Baillot, V. Danos, T. Ehrhard, L. Regnier.(1998)
Timeless Games.
In proceedings of CSL'97, held in Aarhus.
Springer LNCS 1414, Mogens Nielsen and Wolfgang Thomas eds., pp. 5677.
3.7 France Telecom  CNET
3.7.1 Research Directions
In 1999, P.!Chavin worked on an enrichment of CORBAIDL with
operational concepts. C. Bergerot, P. Brisset and J.F. Monin begun to
investigate problems raised by dynamic configurations of interacting
software processes with complex communication and control patterns. As
a typical case study, they consider a planetwide chat services
application. P. Brisset wrote a first version using CML constructs
implemented in Objective Caml. The next step, undertaken by
C. Bergerot and J.F. Monin, is to take profit of a mobile process
approach in order to dynamically reconfigure the routing topology.
3.7.2 Conferences
J.F. Monin and F. presented a paper at FM'99, about a completely
formalized proof of a crucial component for the ATM CAC called ABR.
They also presented a tutorial on formal methods in telecommunications
at the same conference.
3.7.3 Publications

[MKl99]
 JeanFrançois Monin and Francis Klay,
``Correctness Proof of the Standardized Algorithm for ABR
Conformance'', FM'99  Formal Methods, LNCS 1708, Springer Verlag",
ed. Jeannette Wing and Jim Woodcock and Jim Davies, pp 662681, 1999
3.8 ICL
3.8.1 Research Directions
The ICL framework in Agents and Mobility described in PPR1 and PPR2
is running well with a number of different activities,
still encouraging ICL businesses to take part in
the research process from an early stage to ensure they are prepared
for knowledge and technology transfer as results emerge.
The ICL participation in CONFER2 is one of the framework activities.
The virtual laboratory in collaboration with Fujitsu Laboratories, run
as part of the framework, is very much a working reality now. Ideas
are exchanged on the mailing list together with updates on relevant
issues. Other parts of the Fujitsu Family have now joined the virtual
laboratory.
Recently the focus has been on the KafkaPathwalker technology from
Fujitsu Laboratories. KafkaPathwalker is a distributed multiprocess
and agent/action Java based programming library based on a distributed
message queuing system. KafkaPathwalker draws upon ideas from higher
order process calculi and concurrent functional programming from
languages such as April and Facile.
A major project finished this year, demonstrating how agent technology
could be used to enhance webcomputing products from Fujitsu's
TeamWARE group by integration of agent technology into their core
architecture, called Phoenix. The resulting system is called Agent
Enhanced Phoenix. This technology is now scheduled for
productization.
At ICL we have used this technology for building
demonstrators of how agent technology can be used in real world
scenarios. A very successful demonstrator built around the scenario of
``Intelligent Knowledge Management for Engineering in ICL'' has helped
ICL Businesses understand the potential of the technology. There are
now plans for making the technology part of the ICL solution kit and
applying it in major projects.
Close interaction with the developers of the KafkaPathwalker
technology in Fujitsu Laboratories and the developers of Phoenix in
TeamWARE Group ensures transfer of ideas, also from the CONFER2
context, and feedback from prototype development will hopefully make
systems more flexible and better targeted towards future applications.
Last year we reported on work on transferring ideas from the Facile
system to the Java world via the MLj (ML to Java Virtual Machine code)
compiler (which has now moved home from Persimmon to Microsoft
Research in Cambridge). We have succeeded in building the Facile
concurrency primitives in MLj. However, work on the Facile
distribution primitives has not progressed as quickly as anticipated
due to other commitments. In the coming year we hope to use the
KafkaPathwalker library as a transport layer in developing the Facile
distribution primitives in MLj. KafkaPathwalker already implements
many of the necessary facilities for sending and receiving arbitrary
values including higher order objects.
In addition to the technical work relevant to CONFER2 Lone Leth Thomsen
and Bent Thomsen have assisted JeanJacques Levy in the management of
the working group.
3.8.2 Exchange of Personnel
Lone Leth Thomsen and Bent Thomsen participated in the 5th CONFER2
workshop in Pisa (University of Pisa) 29.03.99  31.03.99.
3.8.3 Publications
In the second year of CONFER2 the group at ICL involved in the working
group has produced two relevant publications:

[LTL99]

J.J. Lévy, B. Thomsen, L. Leth:
``Second Year Report for Esprit Working Group 21836 CONFER2
CONcurrency and Funstions: Evaluation and Reduction'',
EATCS Bulletin Number 67 February 1998 pp. 3551.
 [DPLB99]

P. Degano, C. Priami, L. Leth, B. Thomsen:
``Causality for Debugging Mobile Agents'',
accepted for publication in ACTA INFORMATICA, 1999.
3.9 INRIARocquencourt
3.9.1 Research directions
INRIA Rocquencourt has worked in the following directions.
 Distributed JoinCalculus.
The implementation of the Join calculus is being pursued, under
Jocaml. (see join.inria.fr)
 Concurrency and Security
In collaboration with M. Abadi (Compaq SRC  Lucent Technology),
C. Fournet (on leave for Microsoft Research, Cambridge) and
G. Gonthier give a semantics for abstractions of secure cryptographic
protocols, and prove their correctness. Usually, security is described
by informal and global statements, and needs a formal definition
consistent with the semantics of programming languages. By providing a
set of highlevel primitives inside a programming language, one allows
automatic properties such as secrecy and authentication. The proof of
security is reduced to the proof of a full abstraction theorem between
the highlevel programming language with security primitives and the
implementation language. Moreover, this proof demonstrates how a
secure implementation of such a programming language can be built on
top of the join calculus.
As a first example, the case of the private communication channels of
the join calculus is studied. The security of the implementation may
be transparently achieved by a set of interface modules between each
principal and the network, instead of providing a special compiled
version of each principal.
For authentication, a new notion of principal is added to the
highlevel language. It gives two new interesting features: firstly,
the expressivity of the highlevel language is augmented and for
instance may contain statements about access control policies (with
mere channels, one is usually restricted to capabilities); secondly it
allows again efficient implementations. This latter point is rather
surprising and comes from the small number of cryptographic operations
which now are simple multiplexers for all operations between
principals.
The two versions of this work are being submitted (long version) or
presented at POPL'2000 (conference version).
 Distributed Ambients
C. Fournet, J.J. Lévy, and A. Schmitt studied the distributed
implementations for the CardelliGordon's Ambient calculus. This
framework is a very simple and esthetic model of concurrent processes
with mobility. However it has no distributed implementation until
now. Using Jocaml, an asynchronous, distributed implementation may be
designed. It relies on small protocols with several steps for
implementing each of the atomic step of the Ambient calculus. A
translation of Ambients into the join calculus provides a Jocaml
implementation for Ambients. Although this implementation is a simple
prototype, its efficiency is rather good, since it is bases on pure
asynchrony. The corresponding implementation has been presented at
MOS'99 by C. Fournet and A. Schmitt, and a paper describing its theory
is being submitted.
 Objects
This year, Fournet, Maranget, Laneve (Bologna) and Rémy pursued
their work on distributed objects.
 Security and Flow analysis
S. Conchon and F. Pottier consider data dependency and flow analysis
in the lambda calculus to express interference between lambda
terms. This study can be extended to concurrent processes, such as the
Join calculus.
3.9.2 Persons and exchanges
INRIA Rocquencourt participants are JeanJacques Lévy, Fabrice le
Fessant, Sylvain Conchon, Georges Gonthier, Luc Maranget, and Didier
Rémy. A new PhD student, Alan Schmitt, joined our group this year.
From Cambridge, we had regular visits by Cédric Fournet, a one month
visit by James Leifer, and from Bologna several visits by Cosimo
Laneve.
3.9.3 Publications

[AFG99a]

Martín Abadi, Cédric Fournet, and Georges Gonthier.
Secure implementation of channel abstractions.
à paraître, 1999.
 [AFG99b]

Martín Abadi, Cédric Fournet, and Georges Gonthier.
A topdown look at a secure message.
In Proc. of the 19th Foundations of Software Technology and
Theoretical Computer Science, Chennai, December 1999.
 [AFG00]

Martín Abadi, Cédric Fournet, and Georges Gonthier.
Authentication primitives and their compilation.
In 27th ACM SIGPLANSIGACT Symposium on Principles of
Programming Languages. ACM Press, January 2000.
 [FLS99]

Cédric Fournet, JeanJacques Lévy, and Alan Schmitt.
A distributed implementation of ambients.
1999.
à paraître.
 [FS99]

Cédric Fournet and Alan Schmitt.
An implementation of Ambients in JoCAML.
In 5th Mobile Object System Workshop: Programming Languages for
Wide Area Networks, June 1999.
 [lF99]

Fabrice le Fessant.
Jocaml.
available at , 1999.
 [LM99]

JeanJacques Lévy and Luc Maranget.
Explicit substitutions and programming languages.
In Proc. of the 19th Foundations of Software Technology and
Theoretical Computer Science, Chennai, December 1999.
3.10 INRIASophia
3.10.1 Participation to CONFER Workshops and expenses
M. Merro, R. Amadio, G. Boudol, C. Lhoussaine, S. Dal Zilio
attended the CONFER II workshop in Pisa.
Some CONFER money has been used for visits of I. Castellani to
Hennessy's group in Sussex (1 week), and D. Sangiorgi to Walker's
group in Oxford (2 weeks). D. Sangiorgi has also visited Pisa, to
continue a collaboration with F. Levi.
3.10.2 Joint works
Boudol has collaborated with Curien and Lavatelli (ENS Paris),
producing the joint work [BCL99].
F. Levi (Pisa) has spent about 10 months as a postdoc at Sophia. A
collaboration with D. Sangiorgi has produced [LS00].
3.10.3 Research directions
The work conducted this year by the Sophia group can be divided into a
part on semantics and expressiveness, and a part on distribution and
types.
Semantics and expressiveness
Merro [Mer99], developing work carried out last year in Sophia
and Sussex, has given a labeled characterization of barbed congruence
in asynchronous pcalculus, which, unlike previous
characterizations, does not use the matching construct. In absence of
matching the observer cannot directly distinguish two names. In
asynchronous pcalculus the fact that two names are
indistinguishable can be modeled by means of Honda and Yoshida's
notion of equator. The labeled characterization is based on such
a notion. As an application of the theory a fullyabstract encoding
w.r.t. barbed congruence of external mobility (communication of
free names) in terms of internal mobility (communication of
private names) is provided.
Merro, together with Hüttel, Kleist, and Nestman (Aalborg, Denmark)
[NHKM99] has also continued his work on distributed objects
based on Cardelli's Obliq, a lexically scoped, distributed,
objectoriented programming language. In Obliq, object migration was
suggested as the creation of a copy of an object's state at the target
site, followed by turning the object itself into an alias, also called
surrogate, for the remote copy. The creation of object
surrogates as an abstraction of the abovementioned style of migration
is considered. Ojeblik, a distributionfree subset of Obliq, is
introduced and three different configurationstyle semantics, which
only differ in the respective aliasing model, are provided. It
is shown that two of the semantics, one of which matches Obliq's
implementation, render migration unsafe, while a new proposal for a
third semantics is provably safe. This work suggests a
straightforward repair of Obliq's aliasing model such that it allows
programs to safely migrate objects.
Sangiorgi, in a collaboration with Röckl (Technische Universität
München) [RS99], has studied the use of the pcalculus
for semantical descriptions of languages such as Concurrent
Idealised Algol (CIA), combining imperative, functional and
concurrent features. First an operational semantics for CIA has been
produced, given by SOS rules and a contextual form of behavioral
equivalence; then a pcalculus semantics. As behavioral
equivalence on pcalculus processes the standard (weak early)
bisimilarity has been chosen. The two semantics have been compared,
demonstrating that there is a close operational correspondence between
them and that the pcalculus semantics is sound. This allows for
applying the pcalculus theory in proving behavioral properties
of CIA phrases. For this, laws and examples which have served as
benchmarks to various semantics have been used, as well as a more
complex example involving procedures of higher order. By means of
counterexamples it is shown that the pcalculus semantics is not
complete, and discussed how these counterexamples can be dealt with by
adopting refined forms of pcalculus types and, correspondingly,
typed versions of bisimilarity.
Sangiorgi has written a tutorial paper [San99a] on the
comparison between the
firstorder and the
higherorder paradigms for the representation of
mobility in process calculi. The prototypical calculus in the
firstorder paradigm is the pcalculus. In this work, an
asynchronous pcalculus (Lp) that may be regarded as the basis
of some experimental programming languages (or proposal of programming
languages) like Pict, Join, Blue has been taken. The calculus has
then been extended so to allow the communication of higherorder
values, that is values that may contain processes, and it has been
shown that the extension does not add expressiveness: the resulting
higherorder calculus can be compiled down into the original calculus
Lp. Although the paper is mostly a tutorial, it contains some
original contributions. The main one is the full abstraction proof,
which, with respect to previous proofs, is simpler and does not rely
on certain nonfinitary features of the languages such as infinite
summation. Another contribution is the study of optimizations of the
compilation, with which: recursive types can be handled; full
abstraction can be proved also for strong behavioral
equivalences.
The Blue calculus is a direct extension of both the lambda and the pi
calculi. Dal Zilio [DZ99a] has defined an equivalence
for this calculus based on barbed congruence, and proved the validity
of the replication laws. For example, he proves that a replicated
resource, shared by many processes, can be safely copied and
distributed.
Papers written by Boudol in collaboration with Curien and Lavatelli
(ENS Paris) [BCL99], and Sangiorgi [San99b] in previous
years have been revised and will appear in a special issue of
Mathematical Structures in Computer Science in Honour of Roger
Hindley.
Distribution and types
R. Amadio, G. Boudol, C. Lhoussaine [ABL99] have studied an
asynchronous distributed pcalculus, with constructs for
localities and migration. They have shown that a simple static
analysis ensures the receptiveness of channel names, which, together
with a simple type system, guarantees a local deadlockfreedom
property, that they call message deliverability. This property states
that any migrating message will find an appropriate receiver at its
destination locality. The authors argue that this distributed,
receptive calculus is still expressive enough, by giving a series of
examples illustrating the ``receptive style'' of programming we
have. Finally the authors show that the calculus contains the
p_{1}calculus, up to weak asynchronous bisimulation.
Gerard Boudol and Silvano DalZilio [BDZ99]
have provided a translation of FisherHonsellMitchell's
delegationbased object calculus with subtyping into a lambdacalculus
with extensible records. The target type system is an extension of the
system F^{w} of dependent types with recursion, extensible
records and a form of bounded universal quantification. They have
shown that the translation is computationally adequate, that the
typing rules of FisherHonsellMitchell's calculus can be derived in a
rather simple and natural way, and that the new system enjoys the
standard subject reduction property.
During this year, Silvano Dal Zilio has completed his PhD thesis
[DZ99b]. The thesis focuses on the blue calculus, is a
variant of the polyadic picalculus that directly embeds the notion of
function. In the thesis, Dal Zilio considers a version of the blue
calculus extended with records, and studies whether it provides a good
basis for a typed concurrent programming language with imperative,
higherorder, and object features. He notably studies the modeling of
the functional and object oriented programming idioms, and the
addition of polymorphic typing and inheritance. The thesis is divided
into four parts. The first part consists of a detailed analysis of the
blue calculus and its expressiveness. In the second part, which
includes [DZ99a] discussed above, a behavioral
equivalence based on the classical notion of barbed congruence, and a
labeled bisimulation that is finer than this congruence are defined.
Dal Zilio then uses upto proof techniques to prove the validity of
several algebraic laws like, for example, an analogous of Milner's
replication theorem for the picalculus.
In the third part, Dal Zilio studies type systems for the blue
calculus. Starting from a simple implicit type system that
encompasses both Curry's type system for the lambdacalculus, and
Milner's sorting for the picalculus, he successively proposes three
extensions of increasing complexity. He studies the addition of
subtyping, then parametric polymorphism. In this last case, he also
studies the decidability of the type inference problem. Finally, he
studies an higherorder type system with recursion and a particular
form of bounded universal quantification. This system, that is
suitable for the typing of objects, can be intuitively viewed as a
Curry style presentation of Fsub. He proves the soundness of this
system.
The last part of the thesis is devoted to the study of objects in the
blue calculus, and is based on [BDZ99]
discussed above. Dal Zilio gives a typed interpretation of two
popular object calculi, namely AbadiCardelli's object calculus  in
its functional version, and in its concurrent version , and the
calculus of extensible objects defined by Fisher and Mitchell. The
main contribution is a typed interpretation of the calculus of
extensible objects that preserves subtyping.
Sangiorgi, in a collaboration with Francesca Levi (University of Pisa)
[LS00] has studied interference in in Cardelli and Gordon's
Mobile Ambients (MA). Two forms of interferences have been
individuated: plain interferences, which are similar to the
interferences one finds in CCS and pcalculus; and grave
interferences, which are more dangerous and may be regarded as
programming errors. To control interferences, the MA movement
primitives are modified. On the new calculus, the Safe
Ambients (SA), a type system is defined that: controls the mobility
of ambients; removes all grave interferences. Other advantages of SA
are: a useful algebraic theory; programs sometimes more robust (they
require milder conditions for correctness) and/or simpler. All these
points are illustrated on several examples.
Amadio, in a collaboration with S. Prasad (Indian Institute of
Technology, Delhi, India) has worked on security aspects of
distributed mobile systems [AP99]. A namepassing calculus is
presented that can be regarded as a simplified pcalculus equipped
with a cryptographic table. The latter is a data structure
representing the relationships among names. The calculus is applied
to the modeling and verification of secrecy and authenticity
properties in cryptographic protocols relying on symmetric shared
keys. Following classical approaches, the verification task is
formulated as a reachability problem and its decidability proved
assuming finite principals and bounds on the sorts of the messages
synthesized by the attacker.
3.10.4 Publications

[ABL99]

R. Amadio, G. Boudol, and C. Lhoussaine.
The receptive distributed pcalculus.
In Proc. Found. Software Tech. and Theoret. Comp. Sci.,
LNCS. SpringerVerlag, 1999.
To appear.
 [AP99]

R. Amadio and S. Prasad.
The game of the name in cryptographic tables.
In Proc. ASIAN'99, LNCS. SpringerVerlag, 1999.
To appear. Also appeared as INRIA Research Report 3733.
 [BCL99]

G. Boudol, P.L. Curien, and C. Lavatelli.
A semantics for lambda calculi with resources.
Journal of Mathematical Structures in Computer Science, 9(4),
1999.
Special Issue on "LambdaCalculus and Logic" in Honour of Roger
Hindley.
 [BDZ99]

Gérard Boudol and Silvano DalZilio.
An interpretation of extensible objects.
In Proc. of FCT '99  12th International Symposium on
Fundamentals of Computation Theory, aug 1999.
 [DZ99a]

Silvano DalZilio.
A bisimulation for the blue calculus.
Technical Report 3664, INRIA, apr 1999.
 [DZ99b]

Silvano DalZilio.
Le calcul bleu: types et objets.
PhD thesis, Université de Nice  SophiaAntipolis, 1999.
 [LS00]

F. Levi and D. Sangiorgi.
Controlling interference in ambient.
In Proc. POPL'00. ACM Press, 2000.
to appear.
 [Mer99]

M. Merro.
On Equators in Asynchronous Namepassing calculi without
Matching.
In I. Castellani and B. Victor, editors, Proc. Express'99,
volume 27 of Electronic Notes in Theoretical Computer Science.
Elsevier, 1999.
 [NHKM99]

U. Nestmann, H. Hüttel, J. Kleist, and M. Merro.
Aliasing models for object migration.
In P. Amestoy, P. Berger, M. Daydé, I. Duff, V. Frayssé,
L. Giraud, and D. Ruiz, editors, EuroPar'99 ParallelProcessing, volume
1685 of LNCS, pages 13531368. SpringerVerlag, 1999.
 [RS99]

C. Röckl and D. Sangiorgi.
A picalculus semantics of Concurrent Idealised ALGOL.
In Proc. Fossacs'99, volume 1578 of LNCS, pages
306322. SpringerVerlag, 1999.
 [San99a]

D. Sangiorgi.
Asynchronous process calculi: the firstorder and higherorder
paradigms (tutorial).
To appear in TCS, 1999.
 [San99b]

D. Sangiorgi.
From l to p, or: Rediscovering continuations.
Journal of Mathematical Structures in Computer Science, 9(4),
1999.
Special Issue on "LambdaCalculus and Logic" in Honour of Roger
Hindley.
3.11 KTH
3.11.1 Research directions
We have explored the expressiveness of the fusion calculus, by showing
that continuations may be removed both from inputs and outputs while
keeping enough expressiveness to encode prefixes and guarded
summation.
In this subcalculus  the fusion calculus of solos  we have
presented two different encodings of the full calculus. The causal
dependency between the prefix and the continuation is encoded first by
the dependency between a match condition and its guarded agent, and
secondly by the dependency between a scoped subject and a
corresponding scope extrusion. In both encodings the causal
dependencies are controlled by fusion effects  the same machinery
cannot be used in the picalculus. Another important factor is that
the calculus is polyadic: an input or output can carry arbitrarily
many objects. In the monadic calculus we strongly conjecture that the
expressiveness of prefixes is strictly greater than that of solos.
3.11.2 Persons and exchanges
During 1999, the following persons have been active within CONFER2:
Joachim Parrow and Björn Victor (Uppsala University).Ê Victor
visited University of Pisa in December 1999.
3.11.3 Publications

[LV99]

Cosimo Laneve and Björn Victor.
Solos in concert.
In J. Wiederman, P. van Emde Boas and M. Nielsen, eds, Proceedings of ICALP '99, volume 1644 of LNCS, pages 513523.
Springer, July 1999.
3.12 Oxford University
3.12.1 Research activity
Work has been done on theory and applications of pcalculus.
The final version of a paper on semantic definition of concurrent
objectoriented programming languages was prepared for publication
[LW99]. The paper explains how a calculus that extends the
pcalculus with firstorder data and higherorder abstractions,
but has only firstorder interaction, can be used to give semantic
definitions that are clear, precise, and tractable.
The paper [QW99a] studies the relationship between synchronous and
asynchronous mobile processes, in the setting of the pcalculus.
A primitive of the pcalculus, inherited from its ancestor CCS, is
a form of handshake communication. This primitive is central to the
tractability of CCS, pcalculus, and many other theories
of concurrent systems that are based on similar operators.
On the other hand, many concurrent systems, especially distributed
systems, use forms of asynchronous communication, in which the act of
sending a datum and the act of receiving it are separate. Relatedly,
many languages for programming concurrent or distributed systems have
asynchronous primitives, an important reason for this being that they
are amenable to efficient implementation. Language features for
synchronized communication are often implemented using asynchronous
primitives.
The pcalculus has a subcalculus (the asynchronous pcalculus)
in which communication can be understood as asynchronous. The theory
of the asynchronous subcalculus is much less tractable than that of
the pcalculus. It is the subcalculus, however, that is the basis
for concurrent programming language Pict; and the join language is
based on the join calculus, an asynchronous calculus that is closely
related to the asynchronous pcalculus.
The paper is concerned with the effect on behavioral equivalence of
the standard translation from the pcalculus to the asynchronous
pcalculus. It introduces a type system for terms of the target
language (the monadic asynchronous pcalculus), and uses it to
prove a fullabstraction theorem. The theorem states that two
processes of the polyadic pcalculus are typed barbed congruent
iff their translations into the subcalculus are asynchronous monadic
typed barbed congruent.
The paper develops techniques introduced in [QW99b], and builds
on earlier work on types for mobile processes, a topic that is
important both for programming mobile systems and for analysing their
behaviors.
3.12.2 Workshops and site visits
WorkingGroup funds were used to support the participation of David
Walker in the Pisa workshop in March 1999. It is intended that they
will also have supported the cost of accommodation for a visit to
Oxford by Davide Sangiorgi from INRIA Sophia Antipolis where the main
focus of interaction was joint work on pcalculus. (The bill for
this accommodation has not yet been received.)
3.12.3 Publications

[LW99]

X. Liu and D. Walker,
Concurrent objects as mobile processes,
in Proof, Language, and Interaction,
editor G. Plotkin,
MIT Press (to appear).
 [QW99a]

P. Quaglia and D. Walker,
On synchronous and asynchronous mobile processes,
submitted for publication.
 [QW99b]

P. Quaglia and D. Walker,
On encoding pp in mp,
in Proceedings of Foundations of Software Technology and
Theoretical Computer Science, December 1998,
SpringerVerlag Lecture Notes in Computer Science,
vol. 1530, 4253.
3.13 Università di Pisa
3.13.1 Outline
The major line of research of the group at the Dipartimento di Informatica,
Università di Pisa, has been in the areas of Calculi,
Foundational Models and Abstract Machines and Programming
Languages.
 Calculi
The HistoryDependent automata (HDAutomata) model has been further
developed. In particular, it has been addressed the problem of
verifying behavior of asynchronous name passing calculi. An algorithm
to verify asynchronous bisimilarity for finitary pcalculus
processes has been developed.
We propose a specification language for distributed mobile systems
based on asynchronous communication. The language is designed to
support the composition of specifications: it allows to express the
global properties of a system in terms of the local properties of its
components and of coordination patterns. A preliminary work attemps
at providing a refinement framework to deal with security issues.
 Foundational Models and Abstract Machines
Some foundational models, namely rewriting logic, action
calculi and tile logic, have been compared. For each of
these logics we first try to understand their foundations, then we
briefly sketch some applications. The overall goal of is to find out
a common layout where these logics can be recasted, thus allowing for
a comparison and an evaluation of their specific features.
Research has continued on developing mathematical foundations of the
tile model. The natural targets of the tile approach are distributed
mobile systems which are compositional in both space and time. An
executable specification of tile systems has been developed. This has
been obtained by mapping tile logic back into rewriting logic. In
particular, this implementation requires the development of a
metalayer to control rewritings, i.e., to discard computations that do
not correspond to any deduction in tile logic. Our methodology is
applied to term tile systems that cover and extend a
wideclass of SOS formats for the specification of process
calculi. The case study of full CCS, where the term tile format is
needed to deal with recursion (in the form of the replicator
operator), is discussed in detail.
We introduced the notion of cartesian closed double category to
provide mobile calculi for communicating systems with specific
semantic models: One dimension is dedicated to compose systems and the
other to compose their computations and their observations. Also,
inspired by the connection between simply typed lcalculus and
cartesian closed categories, we define a new typed framework, called
double lnotation, which is able to express the
abstraction/application and pairing/projection operations in all
dimensions. In this development, we take the categorical presentation
as a guidance in the interpretation of the formalism. A case study of
the pcalculus, where the double lnotation
straightforwardly handles name passing and creation, concludes the
presentation.
Zerosafe nets have been introduced to extend classical Petri
nets with a primitive notion of transition coordination. To
this aim, besides ordinary places, called stable, zerosafe
nets are equipped with zero places, which cannot contain any
token in a stable marking . An evolution between two stable markings
is called transaction and can be a complex computation that
involves zero places, with the restriction that no stable token
generated in a transaction can be reused in the same transaction. The
abstract counterpart of a generic zerosafe net B consists of an
ordinary PT net whose places are the stable places of B, and whose
transitions are the transactions of B. The two nets offer the
refined and the abstract model of the same system, where the former
can be much smaller than the latter, because of the transition
coordination mechanism. Depending on the chosen approach 
collective vs individual token philosophy  two
notions of transaction may be defined, each leading to different
operational and abstract models.
 Programming Languages
Research has been continued on developing both the implementation and
the theoretical foundations of the experimental programming language
Klaim (Kernel Language for Agents Interaction and Mobility). The
Klaim language, by making use of notions of code mobility, gives the
possibility of coordinating the activity of processes running on a
net. Klaim security architecture exploits a capabilitybased type
system to provide mechanisms for specifying and enforcing policies
that control uses of resources and authorize migration and execution
of processes. Several programming examples illustrate the expressive
power and the flexibility of Klaim type system to support the
specification of control policies and their enforcement. Finally, a
prototype implementation of Klaim in Ada95, has been also
developed.
3.13.2 Perspective
A strong interaction is expected between the work on tiles and the
more applied development on languages for mobile computing. We intend
to provide the mathematical foundations of existing calculi by
exploiting tile logic and its higher order version. Moreover, research
is under way to develop a process calculus representation of the KLAIM
language in order to define notions of observations and of behavioral
equivalences as a basis for verification. We also intend to check the
theoretical developments by designing and implementing suggestive case
studies, taking advantage of the KLAIM prototype.
About verification, we plan to extend the HDautomata techniques to
the analysis of security protocols specified in the secure
pcalculus. Moreover, we intend to address the problem of
developing a specification logic for open and untrusted dynamic
networks and its model checking techniques.
We are interested to further the develop theoretical foundations of
HDautomata and the corresponding verification techniques. One aspect
that we intend to study is the development of efficient verification
methods for checking observational (bisimulation) semantics for
classes of mobile calculi.algorithms for HDautomata
The foundational work on tiles will continue studying the double
lnotation associated to their cartesian closed version.
Preliminary results about the early version of the pcalculus show
the adequacy of this notation for modeling name passing and creation
in a straightforward way. Also the obvious connections between
coalgebras and tiles (which naturally define compositional transition
systems and are already equipped with bisimulation equivalences and
congruences) will be studied.
3.13.3 Persons
The group at Pisa involved in the project consists of Ugo Montanari,
Gianluigi Ferrari, Roberto Bruni and Emilio Tuosto. A PhDstudent,
Emilio Tuosto, under the supervision of Ugo Montanari and Gianluigi
Ferrari, is working on topics which are closely related to the aims of
the CONFER 2 Working Group.
3.13.4 Publications

[BM99a]

Bruni, R. and Montanari, U., ZeroSafe Nets: Composing Nets via
Transition Synchronization, Int. Colloquium on Petri Net Technologies
for Modelling Communication Based Systems, 1999, Fraunhofer
Gesellschaft ISST.
 [BMM99]

Bruni, R. and Meseguer, J. and Montanari, U., Executable Tile
Specifications for Process Calculi, FASE'99, Fundamental Approaches to
Software Engineering, LNCS 1577, 1999.
 [BMMS99]

Bruni, R. and Meseguer, J. and Montanari, U. and Sassone, V.,
Functorial Semantics for Petri Nets under the Individual Token
Philosophy, Category Theory and Computer Science, Elsevier ENTCS 29,
1999.
 [BM99b]

Bruni, R. and Montanari, U., Cartesian Closed Double Categories,
their LambdaNotation, and the PiCalculus, LICS'99, 14th Annual IEEE
Symposium on Logic in Computer Science, IEEE Computer Society, 1999.
 [CFP99]

F. Corradini, G. Ferrari and M. Pistore.
On the Semantics of Durational Actions.
Theoretical Computer Science, to appear 1999.
 [NFP99]

R. De Nicola, G. Ferrari, and R. Pugliese.
Types as Specification of Access Policies
In Secure Internet Programming: Security Issues for
Distributed and Mobile Objects,
LNCS StateOfTheArtSurvey (J. Vitek and C. Jensen Eds.),
LNCS 1603, 1999.
 [NFPV99]

R. De Nicola, G. Ferrari, R. Pugliese and B. Venneri.
Types for Access Control.
In Theoretical Computer Science, to appear.
 [FMSS99]

Ferrari, G., Montangero, C., Semini, L. and Semprini, S.
A Refinement Calculus for Mobility: Expressing
Security Policies, In Proc. OOPSLA
Distributed Object Security Workshop, 1999.
 [GM99]

F. Gadducci, U Montanari.
Comparing Logics for Rewriting:
Rewriting Logic, Action Calculi
and Tile Logic.
Submitted to a special issue of Theoretical Computer Science, 1999.
 [MP99]

Montanari , U. and Pistore, M.
Finate State Verification for the Asynchronous pcalculus.
In Proc. TACAS'99, LNCS 1579, 1999.
 [Tu99]

Tuosto, E.
An Ada95 Implementation of a Network Coordination Language with
Code Mobility,
AdaEurope International Conference on Reliable Software Technologies
Santander, Spain, June 1999
3.13.5 Networking
A CONFER2 workshop has been hold in Pisa from March 29
to March 31. The program of the workshop is
reported below.
3.14 University of Sussex
3.14.1 Research directions
Asynchronous Mobile Processes
Although asynchronous languages have recently become popular, at least
as vehicles for implementation initiatives, there has been very little
success in developing behavioral theories for such languages. As a
step in this direction we investigated an asynchronous version of CCS
and have found an equational inference systems which characterizes
both may and must testing preorders for this language. Our hope is to
extend this to the more expressive asynchronous picalculus.
See CH98 for details.
Types for Distributed Processes
During this period we investigated the use of types to ensure locality
of resources in distributed systems. The research, reported in
YH99 below, was carried out in a higherorder version of the
picalculus, augmented with the primitives from the callbyvalue
lambdacalculus, in which there is also a primitive notion of
location. We showed that it was possible to extend existing IOtype
systems for the picalculus to ensure that all resources (in this case
modeled by picalculus channels), even those created dynamically,
can be serviced at at most one location.
Higherorder behavioral equivalences
One major problem in developing behavioral theories for higherorder
distributed calculi is the interaction between new name generation and
functional abstraction. This interaction can be studied, in isolation
from other distributed concepts, within an apparently very simple
language called the nucalculus, which consists of the lambdacalculus
augmented with new name generation. In JR99 below it is shown that
by adding assignment to this language bisimulation equivalence
coincides with contextual equivalence.
It is hoped that further work along these lines will help illuminate
bisimulation equivalence for higherorder distributed languages.
3.14.2 Personnel and Exchanges
The personnel at the University of Sussex who were actively involved
in Confer2 related research during the period covered by the progress
report are Matthew Hennessy, Julian Rathke, Nobuko Yoshida.
Confer2 resources were used to fund a research visit by Matthew
Hennessy to INRIASophiaAntipolis and to fund a research visit by
Ilaria Castellani, from INRIASophiaAntipolis to Sussex. In addition
it supported (with permission) the attendance by Matthew Hennessy and
Julian Rathke at the workshop HOOTS99.
3.14.3 Publications

[CH98]

Ilaria Castellani and Matthew Hennessy.
Testing theories for asynchronous languages.
In V Arvind and R Ramanujam, editors, 18th Conference on
Foundations of Software Technology and Theoretical Computer Science (Chennai,
India, December 1719, 1998), lncs. sv, December 1998.
 [Hen99]

Y. Yoshida M. Hennessy.
Subtyping and locality in distributed higher order mobile processes
(extended abstract).
In CONCUR '99. SpringerVerlag, 1999.
Full version available as Computer Science Technical Report 1/99,
University of Sussex, 1997. Available from
http://www.cogs.susx.ac.uk/.
 [JR99]

A. Jeffrey and J. Rathke.
Towards a theory of bisimulation for local names.
In Proc. LICS'99, 14^{th} Annual Symposium on Logic in
Computer Science, Trento, pages 5666. IEEE Computer Society Press, 1999.