A Distributed Pi-Calculus

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