[Prev][Next][Index][Thread]
announcement book on the pi-calculus
We are pleased to announce the book:
-------------------------------------------------------
The Pi-Calculus: A Theory of Mobile Processes
Davide Sangiorgi and David Walker
Cambridge University Press, 592 pp, ISBN 0521781779
-------------------------------------------------------
Below is the blurb and the table of contents. For more information, see:
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/Book_pi.html
For the CUP press display and order information, see:
http://uk.cambridge.org/order/WebBook.asp?ISBN=0521781779
Best regards,
Davide Sangiorgi, David Walker
BLURB (from the cover page)
===========================
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.
TABLE OF CONTENTS
=================
Foreword ix
Preface xi
General Introduction 1
Part I : The pi-calculus 5
Introduction to Part I 7
1 Processes 11
1.1 Syntax 11
1.2 Reduction 17
1.3 Action 36
1.4 Basic properties of the transition system 44
2 Behavioural Equivalence 54
2.1 Strong barbed congruence 54
2.2 Strong bisimilarity 64
2.3 Up-to techniques 80
2.4 Barbed congruence 92
Notes and References for Part I 118
Part II : Variations of the pi-calculus 121 Introduction to Part II 123
3 Polyadicity and Recursion 127
3.1 Polyadicity 127
3.2 Recursion 132
3.3 Priority-queue data structures 138
3.4 Data as processes 145
4 Behavioural Equivalence, continued 154
4.1 Distinctions 154
4.2 Variants of bisimilarity 157
4.3 The late transition relations 158
4.4 Ground bisimilarity 162
4.5 Late bisimilarity 164
4.6 Open bisimilarity 166
4.7 The weak equivalences 172
4.8 Axiomatizations and proof systems 174
5 Subcalculi 189
5.1 The Asynchronous pi-calculus 189
5.2 Syntax of Api 190
5.3 Behavioural equivalence in Api 194
5.4 Asynchronous equivalences 198
5.5 Expressiveness of asynchronous calculi 203
5.6 The Localized pi-calculus 211
5.7 Internal mobility 215
5.8 Non-congruence results for ground bisimilarity 223
Notes and References for Part II 227
Part III : Typed pi-calculi 231 Introduction to Part III 233
6 Foundations 236
6.1 Terminology and notation for typed calculi 236
6.2 Base-pi 238
6.3 Properties of typing 244
6.4 The simply-typed pi-calculus 247
6.5 Products, unions, records, and variants 249
6.6 Pattern matching in input 255
6.7 Recursive types 257
7 Subtyping 260
7.1 i/o types 261
7.2 Properties of the type systems with i/o 265
7.3 Other subtyping 270
7.4 The priority queues, revisited 272
7.5 Encodings between union and product types 276
8 Advanced Type Systems 281
8.1 Linearity 281
8.2 Receptiveness 288
8.3 Polymorphism 296
Notes and References for Part III 305
Part IV : Reasoning about Processes using Types 309
Introduction to Part IV 311
9 Groundwork 313
9.1 Using types to obtain encapsulation 313
9.2 Why types for reasoning? 316
9.3 A security property 317
9.4 Typed behavioural equivalences 319
9.5 Equivalences and preorders in simply-typed pi-calculi 328
10 Behavioural Effects of i/o Types 329
10.1 Type coercion 329
10.2 Examples 330
10.3 Wires in the Asynchronous pi-calculus 335
10.4 Delayed input 336
10.5 Sharpened Replication Theorems 338
10.6 Proof techniques 340
10.7 Context Lemma 342
10.8 Adding internal mobility 348
11 Techniques for Advanced Type Systems 351
11.1 Some properties of linearity 351
11.2 Behavioural properties of receptiveness 352
11.3 A proof technique for polymorphic types 359
Notes and References for Part IV 365
Part V : The Higher-Order Paradigm 367
Introduction to Part V 369
12 Higher-Order pi-calculus 373
12.1 Simply-typed HOpi 373
12.2 Other HOpi languages 381
13 Comparing First-Order and Higher-Order Calculi 383
13.1 Compiling higher order into first order 383
13.2 Optimizations 397
13.3 Reversing the compilation 408
13.4 Full abstraction 412
Notes and References for Part V 415
Part VI : Functions as Processes 419 Introduction to Part VI 421
14 The lambda-calculus 424
14.1 The formal system 424
14.2 Contrasting lambda and pi 426
14.3 Reduction strategies: call-by-name, call-by-value, call-by-need 429
15 Interpreting lambda-calculi 434
15.1 Continuation Passing Style 434
15.2 Notations and terminology for functions as processes 436
15.3 The interpretation of call-by-value 438
15.4 The interpretation of call-by-name 452
15.5 A uniform encoding 461
15.6 Optimizations of the call-by-name encoding 464
15.7 The interpretation of strong call-by-name 465
16 Interpreting Typed lambda-calculi 469
16.1 Typed lambda-calculus 469
16.2 The interpretation of typed call-by-value 470
16.3 The interpretation of typed call-by-name 474
17 Full Abstraction 477
17.1 The full-abstraction problem 477
17.2 Applicative bisimilarity 478
17.3 Soundness and non-completeness 479
17.4 Extending the lambda-calculus 483
18 The Local Structure of the Interpretations 492
18.1 Sensible theories and lazy theories 492
18.2 Lévy-Longo Trees 493
18.3 The Local Structure Theorem for call-by-name 496
18.4 Böhm Trees 505
18.5 Local structure of the call-by-value interpretation 505
Notes and References for Part VI 507
Part VII : Objects and pi-calculus 513
Introduction to Part VII 515
19 Semantic Definition 517
19.1 A programming language 517
19.2 Modelling examples 522
19.3 Formal definition 528
20 Applications 533
20.1 Some properties of declarations and commands 533
20.2 Proxies 535
20.3 An implementation technique 539
20.4 A program transformation 541
Notes and References for Part VII 546
List of Tables 548
List of Notations 550
Bibliography 562
Index 576