An Innocent Model of Linear Logic by Paul-André Melliès was referenced by Noam in a serendipitious subthread of the "Claiming Infinities" thread.

Here's the abstract:

Since its early days, deterministic sequential game semantics has been limited to linear or polarized fragments of linear logic. Every attempt to extend the semantics to full propositional linear logic has bumped against the so-called Blass problem, which indicates (misleadingly) that a category of sequential games cannot be self-dual and cartesian at the same time. We circumvent this problem by considering (1) that sequential games are inherently positional; (2) that they admit internal positions as well as external positions. We construct in this way a sequential game model of propositional linear logic, which incorporates two variants of the innocent arena game model: the well-bracketed and the non well-bracketed ones.

The introduction goes on to refer to to André Joyal's "*Category Y with Conway games as objects, and winning strategies as morphisms, composed by sequential interaction*," and points out that "*it is a precursor of game semantics for proof theory and programming languages*," and is "*a self-dual category of sequential games*." The foreword mentions that the paper goes on to give "*a crash course on asynchronous games*" and then "*constructs a linear continuation monad equivalent to the identity functor, by allowing internal positions in our games, [which] circumvents the Blass problem and defines a model of linear logic*."

Jacques Carette called this paper mind-blowing. My mind-blow warning light already exploded. I'm posting this paper because I know a number of LtUers are interested in these topics, and this way I can buttonhole one of them the next time I see them and ask them to explain it to me. ;)

## Recent comments

1 week 2 days ago

1 week 4 days ago

1 week 4 days ago

1 week 5 days ago

1 week 6 days ago

1 week 6 days ago

1 week 6 days ago

1 week 6 days ago

1 week 6 days ago

3 weeks 1 day ago