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

lmcs:4007 - Logical Methods in Computer Science, November 15, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:9)2017
An intensionally fully-abstract sheaf model for $\pi$ (expanded version)Article

Authors: Clovis Eberhart ; Tom Hirschowitz ; Thomas Seiller

    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.


    Volume: Volume 13, Issue 4
    Published on: November 15, 2017
    Accepted on: October 31, 2017
    Submitted on: October 24, 2017
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • Realizability for classical logic, concurrency, references and rewriting; Funder: French National Research Agency (ANR); Code: ANR-11-BS02-0010

    Consultation statistics

    This page has been seen 1737 times.
    This article's PDF has been downloaded 599 times.