Finding presheaf models for the finite pi-calculus.

Abstract

This thesis provides a fully-abstract (set theoretical) model for the finite pi-calculus with respect to late-bisimulation and late-equivalence relations. This is achieved by amalgamating the works by M. P. Fiore, E. Moggi and D. Sangiorgi, and I. Stark. In their respective works the authors construct categorical models, and define a meta-language in which the finite pi-calculus can be interpreted. We discuss the general properties a categorical model should satisfy to be considered an appropriate model for the finite pi-calculus. In particular, I show that the categorical model based on the syntax provides a fully abstract model for the finite pi-calculus. Finally, I include all the details of the model which were often omitted by the above authors. We extend the discussion by examining alternative categorical constructs for the model of the finite pi-calculus, for example we use doubly closed categories which are a main focus of Bunched Logic by P. W. O'Hearn and D. J. Pym.