A Resource Analysis of the π-calculus

We give a new treatment of the π-calculus based on the semantic theory of separation logic, continuing a research program begun by Hoare and OʼHearn. Using a novel resource model that distinguishes between public and private ownership, we refactor the operational semantics so that sending, receiving, and allocating are commands that influence owned resources. These ideas lead naturally to two denotational models: one for safety and one for liveness. Both models are fully abstract for the corresponding observables, but more importantly both are very simple. The close connections with the model theory of separation logic (in particular, with Brookesʼs action trace model) give rise to a logic of processes and resources.