CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  Publications  \  Technical Report Page Login  
banner bottom
File Top
Models of Name-Passing Systems Based on Coalgebras over Nominal Sets

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.

Institution: Departamento de Informática FCT/UNL ( Portugal )

Date: February, 2007

File Bottom