Phase semantics for light linear logic

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journalArticle

10 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 languageEnglish
Pages (from-to)525-549
Number of pages25
JournalTheoretical Computer Science
Volume294
Issue number3
DOIs
Publication statusPublished - 2003 Feb 18

Fingerprint

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

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

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

In: Theoretical Computer Science, Vol. 294, No. 3, 18.02.2003, p. 525-549.

Research output: Contribution to journalArticle

Kanovich, Max I. ; Okada, Mitsuhiro ; Scedrov, Andre. / Phase semantics for light linear logic. In: Theoretical Computer Science. 2003 ; Vol. 294, No. 3. pp. 525-549.
@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 = "2",
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",

}

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

AN - SCOPUS:0037452393

VL - 294

SP - 525

EP - 549

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 3

ER -