The Pi-Calculus: A Theory of Mobile Processes

Front Cover
Cambridge University Press, Oct 16, 2003 - Computers - 596 pages
Mobile 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
Copyright

Common terms and phrases

Bibliographic information