2026-07-21T03:15:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:15745 2024-03-06T10:56:06Z ddc:004 open_access

Games, Mobile Processes, and Functions Jaber, Guilhem Sangiorgi, Davide λ-calculus π-calculus game semantics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guilhem Jaber and Davide Sangiorgi 2022 Is Part Of LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2022.25 urn:nbn:de:0030-drops-157450 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.25 eng https://creativecommons.org/licenses/by/4.0/legalcode