LLL semantics

[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]


                   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.