Games semantics for full propositional linear logic

19 November 2002

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

Vol. 1 (10436871) , 464-473
https://doi.org/10.1109/lics.1995.523280

Abstract

We present a model of propositional classical linear logic (all the connective except for the additive constants) where the formulas are seen as two person games in which connectives are used as tokens, while the proofs are interpreted as strategies for one player. We discuss the intimate connection between these games and the structure of proofs, and prove a full completeness theorem. The main technical innovation is a "double negation" interpretation of CLL into intuitionistic linear logic.

Keywords

This publication has 8 references indexed in Scilit:

On the symmetry of sequentiality
Published by Springer Nature ,1994
A game semantics for linear logic
Annals of Pure and Applied Logic, 1992
Games and full Completeness for multiplicative Linear Logic
Lecture Notes in Computer Science, 1992
A new constructive logic: classic logic
Mathematical Structures in Computer Science, 1991
Linear logic
Theoretical Computer Science, 1987
Sequential algorithms on concrete data structures
Theoretical Computer Science, 1982
Classically and intuitionistically provably recursive functions
Published by Springer Nature ,1978
Dialogspiele als Semantische Grundlage von Logikkalkülen
Archive for Mathematical Logic, 1968