🚀 go-pugleaf

Date: Thu, 3 Sep 1992 14:13:30 +0100 (BST)

The following paper is now available by anonymous ftp from
theory.doc.ic.ac.uk, in papers/Abramsky. Anyone needing a hard copy
should send me their postal address.

--------

\documentstyle[11pt]{article} 


\begin{document} 
\bibliographystyle{alpha}
\title{Games and Full Completeness for Multiplicative Linear Logic}
\author{Samson Abramsky and Radha Jagadeesan \\
Imperial College.}

\maketitle

\begin{abstract}
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  {\em 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 {\em 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 {\it et al}. 
\end{abstract}

\end{document}