CONCUR 2004 START ConferenceManager    

Asynchronous Games 2: The true concurrency of innocence

Paul-André Melliès

Presented at Fifteenth International Conference on Concurrency Theory (CONCUR 2004), London, England, 31 August - 3 September, 2004


In game semantics, one expresses the higher-order value passing mechanisms of the lambda-calculus as sequences of atomic actions by a Player and its Opponent. 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 lambda-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 lambda-terms from their interleaving semantics 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 lambda-calculus, whose game semantics is formulated as a trace semantics.

START Conference Manager (V2.47.4)