# Mita Logic Seminar (Informal Meeting) Paul-André Melliès\$BGn;N9V1i2q(B

\$BF|;~!'(B 2006\$BG/(B9\$B7n(B15\$BF|!!(B16\$B!'(B00\$B!A(B17\$B!'(B30

\$B>l=j!'(B \$B;0EDElJu%S%k#8(BF\$B?MJ8(BCOE\$B2q5D<<(B \$B!J!v>l=jEyITL@\$JJ}\$O7DBg@5Lg\$N%,!<%I%^%s\$K\$*?R\$M2<\$5\$\$!K(B (JR\$BEDD.1X\$^\$?\$OET1DCO28M@~!K\$+\$i(B \$BELJb(B5\$BJ,(B)
\$B!v7zJ*\$NF~8}\$,>o;~%m%C%/\$5\$l\$F\$*\$j\$^\$9\$N\$G!\$(B \$B%I%"OF\$N%\$%s%?!<%[%s\$K\$F(B7F\$B\$N;vL3<

\$B9V1i Paul-André Melliès (Chargé de Recherches CNRS)

\$B%?%\$%H%k!'(B Game semantics is a 2-dimensional Lawvere theory

\$B%"%V%9%H%i%/%H!'(B About six years ago, I worked with Peter Selinger on the categorical semantics of sequential games and polarized linear logic. We realized at the time that the two lifting operations L and R of game semantics:

-- L lifting an Opponent-starting game with an initial Player move,
-- R lifting a Player-starting game with an initial Opponent move

are adjoint functors, with L left adjoint to R.

In this talk, I will explain how to derive game semantics from the very existence of this adjunction. To that purpose, I will introduce the notion of 2-dimensional Lawvere theory, and show that arena games and innocent strategies define the 2-dimensional Lawvere theory of the particular kind of adjunction generated by a continuation model -- all this explained diagrammatically by string diagrams.

I will conclude my talk by discussing when such an adjunction generates a *-autonomous category, building on ideas by Masahito Hasegawa -- this providing a relevant "categorification" of Jean-Yves Girard's phase space model of linear logic.

\$BLd9g\$;@h!'(B
\$B7DXf5A=NBg3X(B21\$B@\$5*?MJ82J3X8&5f5rE@(B
\$B!V?4\$NE}9gE*8&5f!W%;%s%?! \$B=;=j!'El5~ET9A6h;0ED(B 3-1-7 \$B;0EDElJu%S%k(B 8F
e-mail\$B!'(Bphilosophy at abelard.flet.keio.ac.jp

\$BJ?@.(B18\$BG/(B9\$B7n(B13\$BF|(B