Phase semantics for light linear logic

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journalConference articlepeer-review

11 Citations (Scopus)


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
Issue number3
Publication statusPublished - 2003 Feb 18
Externally publishedYes
EventLinear Logic - Tokyo, Japan
Duration: 1996 Mar 281996 Apr 2

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Phase semantics for light linear logic'. Together they form a unique fingerprint.

Cite this