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. |
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
A-calculus abstraction application argument asynchronous axioms barbed congruence behavioural equivalence bisimulation bound output calculus call-by-name call-by-value Computer Science consider Context Lemma Corollary CPS transform defined definition derivation encoding example Exercise expression fn(P fresh name full bisimilarity Functional Programming grammar ground bisimilarity higher-order i/o types image-finite implies induction infer input prefix instance integers interaction Join Calculus lambda calculus late bisimilarity linear types linear-receptive matching mobility notation Notes in Computer open bisimilarity operator output capability output prefix P₁ P₂ pi-calculus polyadic polymorphic process calculi processes programming languages properties prove receptive recursive types relation Replication Theorems restriction result Section semantics simply-typed strong bisimilarity structural congruence subcalculus substitution subterm subtyping Suppose symmetric relation Table techniques theory transition relations translation tuple type environment type systems typing rules unit untyped variables variant via x wrec X-terms