|Home \ Publications \ Technical Report Page||Login|
Models of Name-Passing Systems Based on Coalgebras over Nominal SetsAbstract:
We introduce a category of name-passing systems as certain coalgebras on the category of nominal sets and show how to define models of the pi-calculus in this category. The name-passing systems considered are basically transition systems with four kinds of transitions, capturing internal, free-output, bound-output and input steps. To deal with names and binding at the model level we rely on the theory of nominal sets of Gabbay and Pitts, with the notion of the support of an element as the abstract counterpart of the set of free names of a term. Bound-output and input are interpreted as parameterizing states with names and are formalized as finitely-supported functions from names to states. In the present framework, the operational semantics of the pi-calculus consists in defining an appropriate name-passing system on the set of process terms. The denotational semantics assigns to each process term an ele- ment of the final name-passing system, where the semantic operations that correspond to the syntactic constructs are defined by coinduction, taking advantage of the finality of the coalgebra. The two semantics are proved equivalent. The model is fully abstract with respect to strong late bisimulation and congruence.