Samson Abramsky

We use games and Logic as a mirror to understand an aspect of the

sequentiality/concurrency distinction. We begin with the simple,

intuitive notion of *polarized games* due to Blass, which prefigured

many of the ideas in Linear Logic, and which can be seen as a polarized

version of ideas familiar from process calculi (synchronization trees,

prefixing, summation, the Expansion theorem). We analyze the `shocking'

fact that this very clear and intuitive idea leads to a non-associative

composition; a kind of incompatibility between a purely sequential
model

and logic in a classical format. Two ways of addressing this issue
have

been found. One is to add an explicit (`non-logical') polarity-flipping

operation, and use the resulting model to interpret a

`hyper-sequentialized' version of sequent calculus, in which the current

focus of attention in the proof is explicitly represented. This is
the

approach taken in Girard's Ludics. The other is to broaden the notion
of

game to encompass `truly concurrent games'. In such games there is
no

longer a global polarization (we can have positions in which both papers

can move concurrently), although there are still local polarizations

(each local decision is made by just one of the players). This idea
of

concurrent games was used by Abramsky and Mellies to give a fully

complete model for Linear Logic in its original form (i.e. not

`hyper-sequentialized'), and indeed the correspondence is with

proof-nets, the `parallel syntax for proof theory' in Girard's phrase.