[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