Author :
Laurent, Olivier
Author_Institution :
Preuves, Programmes et Systemes, CNRS & Paris VII Univ., France
Abstract :
We generalize the intuitionistic Hyland-Ong 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 a game model for polarized linear logic with a definability result. As a consequence this gives a complete game model for various classical systems: LC, λμ-calculus,... for both call-by-name and call-by-value evaluations.
Keywords :
formal logic; game theory; process algebra; λμ-calculus; LC; call-by-name; call-by-value; definability; intuitionistic games; polarized games; polarized linear logic; Computer languages; Computer science; Embedded computing; Logic programming; Polarization; Waste materials;
Conference_Titel :
Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on
Print_ISBN :
0-7695-1483-9
DOI :
10.1109/LICS.2002.1029835