Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas - An intensionally fully-abstract sheaf model for $\pi$ (expanded version)

lmcs:4069 - Logical Methods in Computer Science, November 15, 2017, Volume 13, Issue 4
An intensionally fully-abstract sheaf model for $\pi$ (expanded version)

Authors: Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas

Following previous work on CCS, we propose a compositional model for the $\pi$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, relying on a combinatorial presentation of $\pi$-calculus traces in the spirit of string diagrams.


Source : oai:arXiv.org:1710.06744
DOI : 10.23638/LMCS-13(4:9)2017
Volume: Volume 13, Issue 4
Published on: November 15, 2017
Submitted on: October 24, 2017
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages


Share

Browsing statistics

This page has been seen 32 times.
This article's PDF has been downloaded 10 times.