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

Mitsuhiro Okada

研究成果: Article査読

35 被引用数 (Scopus)

抄録

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.

本文言語English
ページ(範囲)333-396
ページ数64
ジャーナルTheoretical Computer Science
227
1-2
DOI
出版ステータスPublished - 1999 9 28

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル