Polarized games

O. Laurent1
1Preuves, Programmes et Systèmes,CNRS, University of Paris, France

Tóm tắt

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, /spl lambda//spl mu/-calculus,... for both call-by-name and call-by-value evaluations.

Từ khóa

#Polarization #Logic programming #Computer languages #Waste materials #Computer science #Embedded computing

Tài liệu tham khảo

10.1109/LICS.1997.614931 10.1016/S0304-3975(99)00039-0 10.1006/inco.2000.2917 10.1017/S096012950100336X harmer, 1999, Games and full abstraction for nondeterministic languages 10.1016/0304-3975(87)90045-4 10.1017/S0960129500001328 danos, 1995, LKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication, London Mathematical Society Lecture note series, 222, 211 10.2307/2275572 laurent, 2002, Etude de la Polarisation en Logique 10.1109/LICS.1995.523280 laurent, 2002, Polarized proof-nets and ??-calculus, Theoretical Computer Science 10.1007/3-540-48959-2_17 mccusker, 1996, Games and Full Abstraction for A Functional Metalanguage with Recursive Types montelatici, 2001, Pre?sentation axiomatique de the?ore?mes de comple?tude forte en se?mantique des jeux et en logique classique 10.1145/263699.263722 parigot, 1992, ??-calculus: An algorithmic interpretation of classical natural deduction, Lecture Notes in Computer Science, 624, 190, 10.1007/BFb0013061 10.1017/S096012950000311X abramsky, 1997, Call-by-value games, Lecture Notes in Computer Science, 1414, 1, 10.1007/BFb0028004 10.1006/inco.2000.2930 10.1007/3-540-44802-0_14 10.1007/3-540-56287-7_113 10.1016/0168-0072(92)90073-9 10.1109/LICS.1997.614933 10.1109/LICS.1999.782638 10.1016/S0304-3975(99)00047-X 10.1145/351240.351262 curien, 1993, On the symmetry of sequentiality, Lecture Notes in Computer Science, 805, 29