Game semantics: easy as Pi
File(s)
Published version
Author(s)
Castellan, Simon
Stefanesco, Leo
Yoshida, Nobuko
Type
Report
Abstract
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order
programming languages. However, due to the complexity of most game models, game semantics has remained
unapproachable for non-experts.
In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation
to a dialect of the π-calculus, referred to as metalanguage, followed by a semantic interpretation of the
metalanguage into a particular game model. The semantic interpretation is done once and for all; while the
syntactic translation can be defined for a wide range of programming languages without knowledge of the
particular game model used. Reasoning on the interpretation (soundness and adequacy) can be done at the
level of the metalanguage through a sound equational theory, escaping tedious technical proofs usually found
in game semantics. We call this methodology programming game semantics.
We expose the methodology in three steps of increasing expressivity, building on concurrent game semantics
based on event structures. By developing an extension of the existing models to deal with non-angelic
nondeterminism, and nonlinear computation, we can give very accurate models of complex languages by a
simple translation into a typed variant of the π-calculus inspired by Differential Linear Logic. We illustrate
this expressivity on IPA, a higher-order programming language with shared-memory concurrency. By simply
translating it into the metalanguage, we give the first model of IPA, which is (1) causal and (2) adequate for
the usual operational notion of bisimulation — a novel result.
To make the development more concrete, we have built a simple prototype to compute the interpretation of
the target programming language into the metalanguage and games strategies.
programming languages. However, due to the complexity of most game models, game semantics has remained
unapproachable for non-experts.
In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation
to a dialect of the π-calculus, referred to as metalanguage, followed by a semantic interpretation of the
metalanguage into a particular game model. The semantic interpretation is done once and for all; while the
syntactic translation can be defined for a wide range of programming languages without knowledge of the
particular game model used. Reasoning on the interpretation (soundness and adequacy) can be done at the
level of the metalanguage through a sound equational theory, escaping tedious technical proofs usually found
in game semantics. We call this methodology programming game semantics.
We expose the methodology in three steps of increasing expressivity, building on concurrent game semantics
based on event structures. By developing an extension of the existing models to deal with non-angelic
nondeterminism, and nonlinear computation, we can give very accurate models of complex languages by a
simple translation into a typed variant of the π-calculus inspired by Differential Linear Logic. We illustrate
this expressivity on IPA, a higher-order programming language with shared-memory concurrency. By simply
translating it into the metalanguage, we give the first model of IPA, which is (1) causal and (2) adequate for
the usual operational notion of bisimulation — a novel result.
To make the development more concrete, we have built a simple prototype to compute the interpretation of
the target programming language into the metalanguage and games strategies.
Date Issued
2019-01-01
Citation
Departmental Technical Report: 19/3, 2019, pp.1-35
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
35
Journal / Book Title
Departmental Technical Report: 19/3
Copyright Statement
© 2019 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published