************************************************************
***                  E R R A T A                         ***
************************************************************


These errata are based on comments by Davide Sangiorgi and
Vincent Cremet.


************************************************************

*** Section 2.1.2 ***

For simplicity, we present an untyped calculus. However,
with polyadicity one should usually at least adopt some
simple sorting. Values (the objects to be transmitted)
are usually assumed to be distinct from the names (that
is, the communication channels). If the chosen alphabet of
values applied is finite, VP can be easily encoded in pure
CCS, simply by using finite summation for inputs.

In rules C2a-C2c on page 9, sets of names are used in the
restrictions. This choice was motivated by standard syntaxes
for CCS, however it may contrast plain pi-calculus syntax.

On page 14, replace [San95] by [San92].


*** Section 2.2.1 ***
                                 _
Note that in a bound output (#~x)a<~b>, the sequence ~x
is to be interpreted as a set, whereas ~b denotes an
ordered tuple.

Mismatching is often omitted in foundational studies of
the pi-calculus. One reason is that it spoils congruence
results. I have included it nevertheless, for reasons of
completeness. In order to exclude this or other operators
from the formalization in Isabelle/HOL presented in
Chapter 3, I would suggest to use an inductive set including
exactly the desired processes. Such a predicate can be
defined in the lines of the well-formedness predicate (see
Section 3.1.2) which is necessary anyway to eliminate exotic
terms.

*** Section 2.3.1 ***

In Table 2.7, compl should be defined as follows:

constdefs
  compl :: "'a labels => 'a labels"
 "compl l == case l of nm a => conm a | conm a => nm a"


************************************************************

*** Section 4.1.3 ***

Paragraph about behavioural equivalence: Remove truncated
sentence.

*** Section 4.2.1 ***

The auxiliary encoding is introduced as a proof-technique
to abstract from administrative steps in the pi-calculus
encoding, so to obtain a closer relationship between the
original (CIA) syntax and the (auxiliary pi-calculus)
encoding.

*** Section 4.3.1 ***

We have investigated in two proofs, one using up-to-context
reasoning, and the other one without. In that specific case,
the paper-proof using up-to-context reasoning was not much
easier, because the pairs were very well-structured in both
cases, and the contexts did not contribute much behaviour
themselves. It seems as if one might gain a lot more when
applying up-to-context reasoning in cases where the contexts
can exhibit quite a bit of behaviour.

*** Section 4.4 ***

Sorry, duplication of a sentence.


************************************************************

*** Section 5.1 ***

Using sets of names and labels like I do requires a certain
care in the design of these sets. It does not make much
sense, for instance, to include a(x) but not a(y). The
reason for this choice was the greater simplicity of a
formalization.

*** Section 5.2.1 ***

The model of the SWP formalized in this Section uses
incrementation modulo n in order to capture the cyclicity
of the behaviour.

On page 100, L2 should be L1.


************************************************************