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: LC, λμ-calculus, ... for both call-by-name and call-by-value evaluations.
Publié le : 2004-07-05
Classification:
Game semantics,
Linear logic,
Polarities,
Lambda-mu calculus,
Control categories,
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO],
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
@article{hal-00009116,
author = {Laurent, Olivier},
title = {Polarized games},
journal = {HAL},
volume = {2004},
number = {0},
year = {2004},
language = {en},
url = {http://dml.mathdoc.fr/item/hal-00009116}
}