In the early 90s, I adapted Lorenzen's game semantics of logic to give a "geometrical" description of what is going on during cut elimination (interaction between two strategies), obtaining a proof of termination which I believe is essentially different from the one of Gentzen. This introduced the notion of pointer sequence and visibility, which was used later in game semantics of simply typed lambda calculus. The termination argument, published in the proceeding of CLICS 92, was used in P.-L. Curien's paper Abstract Bohm trees , MSCS 8 (1998), to present a general termination argument about abstract machine evaluation of lambda terms (it is not known yet if there is a more direct argument for this termination result). The same argument was then used later in a paper of P. Clairambault and R. Harmer on Totality in Arena Games.

I tried to present a general survey in this talk; in particular, I mention S. Berardi's discovery that the notion of visibility can be extended for infinite games.

Stefano Berardi wrote also some description of this approach with more references.

One can also generalize the game to allow the strategy to play with functions, that are thought of as stating general laws that can be refined by interaction. One gets in this way a natural computational interpretation of dependent choice with classical logic. This was actually Spector's starting point, and similar attempts can be found in the notebooks of Gödel. Using this game semantics, I suggested a realizability interpretation of countable choice. The following paper is an example of what can be done in this direction.

This interpretation has been used by F. Aschieri in this paper where he provides a remarkable refinement of Gentzen's bounds for cut-elimination: the complexity depends on the depth of backtracking of the two interacting strategies.

- An introductory paper (June 91) where I try to describe the problem: how to get a termination proof for cut-elimination by a direct "geometric" description of what is going on, using game semantics

- The original article (March 92) describing interaction between two strategies that can backtrack. (It was published in a much revised form.) Here is a version with slides (March 92).

- The published version (accepted March 93, published in 95) of the previous paper.

Last modified: Fri Sep 13 22:08:32 MET DST 2002