Expressive Power and Type-Based Embedding.

What may be surprising is the fact that the single operation of name passing can single-handedly represent the dynamics of diverse language constructs: procedural calls, sequencing, assignment, exception, object, in addition to communication and concurrency, can all be simply simulated by name passing and their composition. Further, as a result of recent research by three of the co-authors of the present proposal [12,72], we can embed representative classes of programs' behaviour without losing information if we equip the $\pi$-calculus with appropriate type structures (which are closely related to Linear Logic [32] and Game Semantics [1,47] and will sometimes be referred to hereafter as linear/affine types). Technically, a key observation in these embedding results is that name passing offers fine grains of computation which can be organised to represent arbitrary operational behaviour of the known programming constructs. The type structure then offers a discipline by which the fine-grained dynamics and algebra of the $\pi$-calculus are organised to represent those of the object languages. The embeddability extends from procedures to imperative constructs such as state, control and objects to generic computation to concurrency.

A pleasant feature of these embeddings is that the type structures of the $\pi$-calculus place those of programming languages in a more general, symmetric structure, which can then be instantiated into that of each language. Thus the typed $\pi$-calculus gives a self-contained universe which allows independent theoretical studies and which can still be reflected onto individual languages. The articulation given by general type structure also assists tractable development of program analyses at the level of processes, from our experience outlined below.