## The Pi-Calculus: A Theory of Mobile ProcessesMobile systems, whose components communicate and change their structure, now pervade the informational world and the wider world of which it is a part. The science of mobile systems is as yet immature, however. This book presents the pi-calculus, a theory of mobile systems. The pi-calculus provides a conceptual framework for understanding mobility, and mathematical tools for expressing systems and reasoning about their behaviours. The book serves both as a reference for the theory and as an extended demonstration of how to use pi-calculus to describe systems and analyse their properties. It covers the basic theory of pi-calculus, typed pi-calculi, higher-order processes, the relationship between pi-calculus and lambda-calculus, and applications of pi-calculus to object-oriented design and programming. The book is written at the graduate level, assuming no prior acquaintance with the subject, and is intended for computer scientists interested in mobile systems. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Introduction to Part I | 7 |

Processes | 11 |

12 Reduction | 17 |

13 Action | 36 |

14 Basic properties of the transition system | 44 |

Behavioural Equivalence | 54 |

22 Strong bisimilarity | 64 |

23 Upto techniques | 80 |

95 Equivalences and preorders in simplytyped 𝜋calculi | 328 |

Behavioural Effects of io Types | 329 |

102 Examples | 330 |

103 Wires in the Asynchronous 𝜋calculus | 335 |

104 Delayed input | 336 |

105 Sharpened Replication Theorems | 338 |

106 Proof techniques | 340 |

107 Context Lemma | 342 |

24 Barbed congruence | 92 |

Notes and References for Part I | 118 |

II | 121 |

Introduction to Part II | 123 |

Polyadicity and Recursion | 127 |

32 Recursion | 132 |

33 Priorityqueue data structures | 138 |

34 Data as processes | 145 |

Behavioural Equivalence continued | 154 |

42 Variants of bisimilarity | 157 |

43 The late transition relations | 158 |

44 Ground bisimilarity | 162 |

45 Late bisimilarity | 164 |

46 Open bisimilarity | 166 |

47 The weak equivalences | 172 |

48 Axiomatizations and proof systems | 174 |

Subcalculi | 189 |

52 Syntax of A𝜋 | 190 |

53 Behavioural equivalence in A𝜋 | 194 |

54 Asynchronous equivalences | 198 |

55 Expressiveness of asynchronous calculi | 203 |

56 The Localized 𝜋calculus | 211 |

57 Internal mobility | 215 |

58 Noncongruence results for ground bisimilarity | 223 |

Notes and References for Part II | 227 |

III | 231 |

Introduction to Part III | 233 |

Foundations | 236 |

62 Base𝜋 | 238 |

63 Properties of typing | 244 |

64 The simplytyped 𝜋calculus | 247 |

65 Products unions records and variants | 249 |

66 Pattern matching in input | 255 |

67 Recursive types | 257 |

Subtyping | 260 |

71 io types | 261 |

72 Properties of the type systems with io | 265 |

73 Other subtyping | 270 |

74 The priority queues revisited | 272 |

75 Encodings between union and product types | 276 |

Advanced Type Systems | 281 |

82 Receptiveness | 288 |

83 Polymorphism | 296 |

Notes and References for Part III | 305 |

IV | 309 |

Introduction to Part IV | 311 |

Groundwork | 313 |

92 Why types for reasoning? | 316 |

93 A security property | 317 |

94 Typed behavioural equivalences | 319 |

108 Adding internal mobility | 348 |

Techniques for Advanced Type Systems | 351 |

112 Behavioural properties of receptiveness | 352 |

113 A proof technique for polymorphic types | 359 |

Notes and References for Part IV | 365 |

V | 367 |

Introduction to Part V | 369 |

HigherOrder 𝜋calculus | 373 |

122 Other HO𝜋 | 381 |

Comparing FirstOrder and HigherOrder Calculi | 383 |

132 Optimizations | 397 |

133 Reversing the compilation | 408 |

134 Full abstraction | 412 |

Notes and References for Part V | 415 |

VI | 419 |

Introduction to Part VI | 421 |

The 𝜆calculus | 424 |

142 Contrasting 𝜆 and 𝜋 | 426 |

callbyname callbyvalue callbyneed | 429 |

Interpreting 𝜆calculi | 434 |

152 Notations and terminology for functions as processes | 436 |

153 The interpretation of callbyvalue | 438 |

154 The interpretation of callbyname | 452 |

155 A uniform encoding | 461 |

156 Optimizations of the callbyname encoding | 464 |

157 The interpretation of strong callbyname | 465 |

Interpreting Typed 𝜆calculi | 469 |

162 The interpretation of typed callbyvalue | 470 |

163 The interpretation of typed callbyname | 474 |

Full Abstraction | 477 |

172 Applicative bisimilarity | 478 |

173 Soundness and noncompleteness | 479 |

174 Extending the 𝜆calculus | 483 |

The Local Structure of the Interpretations | 492 |

182 LévyLongo Trees | 493 |

183 The Local Structure Theorem for callbyname | 496 |

184 Böhm Trees | 505 |

Notes and References for Part VI | 507 |

VII | 513 |

Introduction to Part VII | 515 |

Semantic Definition | 517 |

192 Modelling examples | 522 |

193 Formal definition | 528 |

Applications | 533 |

202 Proxies | 535 |

203 An implementation technique | 539 |

204 A program transformation | 541 |

Notes and References for Part VII | 546 |

### Common terms and phrases

abstraction action allows application argument asynchronous axioms barbed congruence behaviour bisimilarity bisimulation calculus call-by-name call-by-value closed communication complete components condition consider constructs context continuation Corollary defined definition derivation deſ discussed encoding equality equivalence example Exercise expression extended fact fresh function give given ground Hence holds implies important induction infer input instance interaction introduced iſo language late Lemma linear matching method normal Note object observable obtained occur operator output possible prefix presented programming proof properties prove reason receives receptive recursive reduction reference relation replication represents respect restriction result rules Section semantics similar sorting strong strong barbed structural substitution subtyping Suppose T-calculus Table techniques Theorem theory transform transition translation type environment unit variables variant write