$B;0EDO@M}3X%;%_%J!<(B
Paul-André Melliès $B65

$BF|;~!'(B 1$B7n(B19$BF|(B 13$B!'(B00$B!A(B14$B!'(B30

$B>l=j!'(B $B7D1~5A=NBg3X;0ED%-%c%s%Q%9(B $BEl4[(B5$B3,(B $B%W%m%8%'%/%H<<(B (JR$BEDD.1X!"ET1DCO2

$B9V1i Paul-André Melliès ($B%U%i%s%9!&(BCNRS$B!"%Q%jBh#7Bg3X!&>pJs3X8&5f=j!&(BCharge de recherches ($BF|K\$NBg3X$N=u65

$B%?%$%H%k!'(B ``An introduction to asynchronous game semantics''

$B%"%V%9%H%i%/%H!'(B In game semantics, the higher-order value passing mechanisms of the lambda-calculus are decomposed as sequences of atomic actions exchanged by a Player and its Opponent. Seen from this angle, game semantics is akin to trace semantics in concurrency theory, where a process is identified to the sequences of requests it generates in the course of time. Asynchronous game semantics is an attempt to bridge the gap between the two subjects, and to see mainstream game semantics as a refined and interactive form of trace semantics. Asynchronous games are positional games played on Mazurkiewicz traces, which reformulate (and generalize) the usual notion of arena game. The framework enables to analyze the interleaving semantics of lambda-terms, expressed as innocent strategies, in the perspective of true concurrency. The analysis reveals that innocent strategies are positional strategies regulated by forward and backward confluence properties. A further distinction between external and internal positions in asynchronous games leads to the very first sequential game model of full propositional linear logic -- in the style of Blass games.

$BLd9g$;@h!'(B
$B7DXf5A=NBg3X(B21$B@$5*?MJ82J3X8&5f5rE@!V?4$NE}9gE*8&5f!W%;%s%?!<(B
$B%o!<%/%7%g%C%W;vL36I(B
$B=;=j!'El5~ET9A6h;0ED(B 3-1-7 $B;0EDElJu%S%k(B 8F
e-mail$B!'([email protected]