In game semantics, one expresses the higher-order value passing mechanisms of the λ-calcuIus as sequences of atomic actions exchanged by a Player and its Opponent in the course of time. This is reminiscent of trace semantics in concurrency theory, in which a process is identified to the sequences of requests it generates. We take as working hypothesis that game semantics is, indeed, the trace semantics of the λ-calculus. This brings us to a notion of asynchronous game, inspired by Mazurkiewicz traces, which generalizes the usual notion of arena game. We then extract the true concurrency semantics of λ-terms from their interleaving semantics formulated as innocent strategies. This reveals that innocent strategies are positional strategies regulated by forward and backward interactive confluence properties. We conclude by defining a non uniform variant of the λ-calculus, whose game semantics is formulated as a trace semantics. © Springer-Verlag 2004.
CITATION STYLE
Melliès, P. A. (2004). Asynchronous games 2: The true concurrency of innocence. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3170, 448–465. https://doi.org/10.1007/978-3-540-28644-8_29
Mendeley helps you to discover research relevant for your work.