Phase semantics for light linear logic

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journalConference article

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
EventLinear Logic - Tokyo, Japan
Duration: 1996 Mar 281996 Apr 2

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this