Polarized games

We generalize the intuitionistic Hyland–Ong games (and in a second step Abramsky–Jagadeesan–Malacaria games) to a notion of polarized games allowing games with plays starting by proponent moves. The usual constructions on games are adjusted to fit this setting yielding game models for both Intuitionistic Linear Logic and Polarized Linear Logic. We prove a definability result for this polarized model and this gives complete game models for various classical systems: , λμ-calculus, … for both call-by-name and call-by-value evaluations.