Phase semantics for light linear logic (extended abstract)

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journalArticle

10 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 languageEnglish
Pages (from-to)221-234
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Volume6
DOIs
Publication statusPublished - 1997

Fingerprint

Linear Logic
Phase Space
Semantics
Cut-elimination
Proposition
Completeness
Polynomial time
Refinement
Paradigm
Polynomials

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Phase semantics for light linear logic (extended abstract). / Kanovich, Max I.; Okada, Mitsuhiro; Scedrov, Andre.

In: Electronic Notes in Theoretical Computer Science, Vol. 6, 1997, p. 221-234.

Research output: Contribution to journalArticle

@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",

}

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 - Article

AN - SCOPUS:18944363457

VL - 6

SP - 221

EP - 234

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -