Finding presheaf models for the finite pi-calculus.

摘要

finite π-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 π-calculus can be interpreted. We discuss the general properties a categorical model should satisfy to be considered an appropriate model for the finite π-calculus. In particular, I show that the categorical model based on the syntax provides 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 π-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.