Phase semantics for light linear logic

Max I. Kanovich; Mitsuhiro Okada; Andre Scedrov

doi:10.1016/S0304-3975(01)00177-3

Phase semantics for light linear logic

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journal › Conference article › peer-review

11 Citations (Scopus)

Abstract

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.

Original language	English
Pages (from-to)	525-549
Number of pages	25
Journal	Theoretical Computer Science
Volume	294
Issue number	3
DOIs	https://doi.org/10.1016/S0304-3975(01)00177-3
Publication status	Published - 2003 Feb 18
Externally published	Yes
Event	Linear Logic - Tokyo, Japan Duration: 1996 Mar 28 → 1996 Apr 2

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1016/S0304-3975(01)00177-3

Cite this

@article{dfb96a780d5944efbe5af6f9502db894,

title = "Phase semantics for light linear logic",

abstract = "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.",

author = "Kanovich, {Max I.} and Mitsuhiro Okada and Andre Scedrov",

year = "2003",

month = feb,

day = "18",

doi = "10.1016/S0304-3975(01)00177-3",

language = "English",

volume = "294",

pages = "525--549",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

number = "3",

note = "Linear Logic ; Conference date: 28-03-1996 Through 02-04-1996",

}

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 -

Phase semantics for light linear logic

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this