[Prev][Next][Index][Thread]
paper available by ftp
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}