Distributed Pi-Calculus Book

Preface     ix
Acknowledgements     xvii
Inductive principles     1
Induction     1
Coinduction     4
Bisimulation equivalence     6
The asynchronous Pi-Calculus     10
The language aPi     10
Reduction semantics for aPi     16
An action semantics for aPi     27
A coinductive behavioural equivalence for aPi     34
Contextual equivalences     37
An observational Its for aPi     43
Justifying bisimulation equivalence contextually     47
Questions     52
Types for api     55
Runtime errors     55
Typechecking with simple types     60
Properties of typechecking     65
Types as capabilities     72
Questions     93
Types and behaviour in aPi     96
Actions-in-context for aPi     98
Typed bisimulation equivalence     112
Questions     122
A distributed asynchronous pi-calculus     124
The language aDpi     127
Access control types for aDpi     139
Subject reduction for aDpi     159
Type safety foraDpi     169
Distributed consistency of local channels     185
Questions     191
Behavioural equivalences for aDpi     194
Actions-in-context for aDpi     195
Typed bisimulation equivalence for aDpi     200
Describing bisimulations     202
Servers and clients     215
Modelling a firewall     221
Typed contextual equivalences     226
Justifying bisimulation equivalence contextually in aDpi     230
Questions     242
Sources     244
List of figures     248
Notation     250
Bibliography     254
Index     257