TY - JOUR
T1 - Phase semantics for light linear logic
AU - Kanovich, Max I.
AU - Okada, Mitsuhiro
AU - Scedrov, Andre
PY - 2003/2/18
Y1 - 2003/2/18
N2 - Light linear logic (Girard, Inform. Comput. 14 (1998) 175-204) is a refinement of the propositions-as-types paradigm to polynomial-time computation. A semantic setting for the underlying logical system is introduced here in terms of fibred phase spaces. Strong completeness is established, with a purely 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.
AB - Light linear logic (Girard, Inform. Comput. 14 (1998) 175-204) is a refinement of the propositions-as-types paradigm to polynomial-time computation. A semantic setting for the underlying logical system is introduced here in terms of fibred phase spaces. Strong completeness is established, with a purely 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.
UR - http://www.scopus.com/inward/record.url?scp=0037452393&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0037452393&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(01)00177-3
DO - 10.1016/S0304-3975(01)00177-3
M3 - Conference article
AN - SCOPUS:0037452393
SN - 0304-3975
VL - 294
SP - 525
EP - 549
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 3
T2 - Linear Logic
Y2 - 28 March 1996 through 2 April 1996
ER -