LLL semantics

• To: linear@CS.Stanford.EDU
• Subject: LLL semantics
• From: Andre Scedrov <scedrov@saul.cis.upenn.edu>
• Date: Sun, 24 Nov 1996 12:17:05 -0500 (EST)
• Original-Sender: lincoln@CS.Stanford.EDU

[------- 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. 

• Prev: Paper announcement
• Next: Thesis
• Index(es):
  • Main
  • Thread