Displacement Games as a model of linear logic
Résumé
Given any cartesian closed category (standard model of the lambda calculus), we construct a certain category from it, whose objects we call displacement games, and show it is a model of linear logic (in other words, a *-autonomous category). We show that the construction has points in common with the Dialectica and Chu constructions, but that its closest relative is Läuchli semantics.