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.

### Contents

Preface; Introduction; Part I. The p-Calculus: 1. Processes; 2. Behavioural equivalence; Part II. Variations of the p-Calculus: 3. Polyadicity and recursion; 4. Behavioural equivalence, continued; 5. Subcalculi; Part III. Typed p-Calculi: 6. Foundations; 7. Subtyping; 8. Advanced type systems; Part IV. Reasoning about Processes Using Types: 9. Groundwork; 10. Behavioural effects of i/o types; 11. Techniques for advanced type systems; Part V. The Higher-Order Paradigm: 12. Higher-order p-calculus; 13. Comparing first-order and higher-order calculi; Part VI. Functions as Processes: 14. The l-calculus; 15. Interpreting l-calculi; 16. Interpreting typed l-calculi; 17. Full abstraction; 18. The local structure of the interpretations; Part VII. Objects and p-Calculus: 19. Semantic definition; 20. Applications; List of notations; Bibliography; Index.