The functional view of computation finds perhaps its most serious limitation in the analysis of concurrent systems (cf. chapter 9). The challenge is then to cope with the problems offered by concurrent systems while retaining some of the mathematically brilliant ideas and techniques developed in the pure functional setting.

In this chapter we introduce a simple extension of CCS known as π-calculus. The π-calculus is a rather minimal calculus whose initial purpose was to represent the notion of name or reference in a concurrent computing setting. It turns out that the π-calculus allows us for simple encodings of various functional and concurrent models. It can then be used as a privileged tool to understand in which sense functional computation can be embedded in a concurrent model.

Section 16.1 is dedicated to the introduction of some basic theory of the π-calculus. In section 16.2, we illustrate the expressive power of the π-calculus by encoding into it a concurrent functional language, called λ∥-calculus, that can be regarded as the kernel of concurrent extensions of the ML programming language such as LCS, CML and Facile where an integration of functional and concurrent programming is attempted. In section 16.3, we study the adequacy of the encoding of the λ∥-calculus in the π-calculus.

This chapter presents an operational phenomenon but fails to give a denotational account of it. As this book goes to press, there have been a few attempts in this direction [FMS96, Sta96].