Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic

Mitsuhiro Okada

Research output: Contribution to journalArticle

34 Citations (Scopus)

Abstract

We give a natural extension of Girard's phase semantic completeness proof of the (first order) linear logic Girard (Theoret. Comput. Sci., 1987) to a phase semantic cut-elimination proof. Then we extend this idea to a phase semantic cut-elimination proof for higher order linear logic. We also extend the phase semantics for provability to a phase semantics-like framework for proofs, by modifying the phase space of monoid domain to that of proof-structures (untyped proofs) domain, in a natural way. The resulting phase semantic-like framework for proofs provides various versions of proof-normalization theorem.

Original languageEnglish
Pages (from-to)333-396
Number of pages64
JournalTheoretical Computer Science
Volume227
Issue number1-2
DOIs
Publication statusPublished - 1999 Sep 28

Keywords

  • Cut-elimination
  • Higher-order logic
  • Linear logic
  • Normalization theorem
  • Phase semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic'. Together they form a unique fingerprint.

  • Cite this