[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
PHASE SEMANTICS FOR LIGHT LINEAR LOGIC
M.I. Kanovich, M. Okada, and A. Scedrov
Girard's light linear logic (LLL) is a refinement of the propositions-as-types
paradigm to polynomial-time computation. Although syntax of LLL is well-
understood thanks to Girard's careful analysis, semantics for LLL has remained
an open question. A semantic setting for the underlying logical system is
introduced here in terms of fibred phase spaces. Strong completeness is
established, with a semantic proof of cut elimination as a consequence.
A number of mathematical examples of fibred phase spaces are presented
that illustrate subtleties of light linear logic. It is explained how
(!A tensor !B ) -o !(A tensor B) and 1 -o !1 can fail "in nature".
A paper is available by anonymous ftp from ftp.cis.upenn.edu in the
directory pub/papers/scedrov as fibre.ps or fibre.ps.gz.