We establish a tight connection between two models of the λ-calculus, namely Milner’s encoding into the π-calculus (precisely, the Internal π-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by π and OGS. We do so for various LTSs: the standard LTS for π and a new "concurrent" LTS for OGS; an "output-prioritised" LTS for π and the standard alternating LTS for OGS. We then show that the equivalences induced on λ-terms by all these LTSs (for π and OGS) coincide. These connections allow us to transfer results and techniques between π and OGS. In particular we import up-to techniques from π onto OGS and we derive congruence and compositionality results for OGS from those of π. The study is illustrated for call-by-value; similar results hold for call-by-name.
@InProceedings{jaber_et_al:LIPIcs.CSL.2022.25, author = {Jaber, Guilhem and Sangiorgi, Davide}, title = {{Games, Mobile Processes, and Functions}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {25:1--25:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.25}, URN = {urn:nbn:de:0030-drops-157450}, doi = {10.4230/LIPIcs.CSL.2022.25}, annote = {Keywords: \lambda-calculus, \pi-calculus, game semantics} }
Feedback for Dagstuhl Publishing