a1 Department of Computing, Imperial College of Science, Technology and Medicine, London, SW7 2BZ, England, E-mail: firstname.lastname@example.org
a2 Department of Mathematical Sciences, Loyola University, Chicago, E-mail: email@example.com
We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al.
(Received October 06 1992)
(Revised August 10 1993)