Phase semantics for light linear logic (extended abstract)

Max I. Kanovich; Mitsuhiro Okada; Andre Scedrov

doi:10.1016/S1571-0661(05)80159-8

Phase semantics for light linear logic (extended abstract)

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

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

11 Citations (Scopus)

Abstract

Light linear logic 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)	221-234
Number of pages	14
Journal	Electronic Notes in Theoretical Computer Science
Volume	6
DOIs	https://doi.org/10.1016/S1571-0661(05)80159-8
Publication status	Published - 1997
Externally published	Yes
Event	MFPS XIII, Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference - Pittsburgh, PA, United States Duration: 1997 Mar 23 → 1997 Mar 26

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1016/S1571-0661(05)80159-8

Cite this

@article{b27375a4bc3242eebf4d444f208a3c1a,

title = "Phase semantics for light linear logic (extended abstract)",

abstract = "Light linear logic 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 = "1997",

doi = "10.1016/S1571-0661(05)80159-8",

language = "English",

volume = "6",

pages = "221--234",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

note = "MFPS XIII, Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference ; Conference date: 23-03-1997 Through 26-03-1997",

}

TY - JOUR

T1 - Phase semantics for light linear logic (extended abstract)

AU - Kanovich, Max I.

AU - Okada, Mitsuhiro

AU - Scedrov, Andre

PY - 1997

Y1 - 1997

N2 - Light linear logic 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 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=18944363457&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944363457&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(05)80159-8

DO - 10.1016/S1571-0661(05)80159-8

M3 - Conference article

AN - SCOPUS:18944363457

SN - 1571-0661

VL - 6

SP - 221

EP - 234

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - MFPS XIII, Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference

Y2 - 23 March 1997 through 26 March 1997

ER -

Phase semantics for light linear logic (extended abstract)

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this