Skip to Main content Skip to Navigation
Reports

Concurrent Game Semantics: Easy as Pi

Abstract : Game semantics has proven to be a robust method to give compositional semantics for a variety of programming languages. However, its complexity makes it inaccessible for nonexperts. In this paper, we aim at making game semantics more accessible by decomposing it into two steps. The first is a syntactic translation into a session typed π-calculus, the metalanguage, which explicits a protocol for an open program to communicate with its context. The second is a semantic interpretation of the metalanguage. The syntactic translation can be defined without knowledge of the particular model used, and different models of the metalanguage (traces, partial orders) yield different reasoning powers. Moreover, simple reasoning on the model (soundness and adequacy) can be done at the level of the metalanguage, escaping tedious proofs usually found in game semantics. We call this methodology programming game semantics. We design a metalanguage (π DiLL) inspired from Differential Linear Logic, meant to correspond to strategies in concurrent game semantics. We translate ML , an extension of Mini-ML with shared memory concurrency, into π DiLL and show that the translation is sound and adequate. We then describe a causal and non-angelic game model using event structures, which supports a fully-abstract interpretation of π DiLL. Combining both results, we obtain the first compositional model of a concurrent higherorder language, which is sound and adequate, and fully abstract on second-order terms, for weak bisimulation. We have implemented a prototype which can explore the generated causal object from a subset of OCaml.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/hal-03128187
Contributor : Simon Castellan Connect in order to contact the contributor
Submitted on : Tuesday, February 2, 2021 - 1:13:35 PM
Last modification on : Friday, January 21, 2022 - 3:09:40 AM
Long-term archiving on: : Monday, May 3, 2021 - 6:16:58 PM

File

2011.05248.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03128187, version 1

Citation

Simon Castellan, Léo Stefanesco, Nobuko Yoshida. Concurrent Game Semantics: Easy as Pi. [Research Report] Inria. 2020. ⟨hal-03128187⟩

Share

Metrics

Les métriques sont temporairement indisponibles