We apply the recently developed techniques of higher order abstract syntax and functorial operational semantics to give a compositional and fully abstract semantics for the pi-calculus equipped with open bisimulation. The key novelty in our work is the realisation that the sophistication of open bisimulation requires us to move from the usual semantic domain of presheaves over subcategories of Set to presheaves over subcategories of Rel. This extra structure is crucial in controlling the renaming of extruded names and in providing a variety of different dynamic allocation operators to model the different binders of the pi-calculus.
Note: Accepted for CMCS 2004
Available as Postscript (927 kB), PDF (293 kB), and compressed Postscript (356 kB)
Download BibTeX entry.