The pi-calculus: a Theory of Mobile Processes Davide Sangiorgi, INRIA Sophia Antipolis David Walker, University of Oxford 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