Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs (Extended Abstract)

Mitsuhiro Okada

研究成果: Article査読

12 被引用数 (Scopus)

抄録

We give a natural extension of Girard phase semantics of the linear logic [1] to the classical and intuitionistic higher order linear logics and give a uniform phase-semantic proof of the higher order cut-elimination theorem as well as the completeness theorem. Although our proof in this paper is mainly concentrated on the framework of linear logic, the proof technique works for various different logical systems uniformly, too. We also extend our phase semantics for provability to phase semantics for proofs, by modifying the phase space of monoid domain to that of proofs domain, in a natural way. The resulting phase semantics for proofs provides various versions of proof-normalization theorem. The details of this extension will appear in the full-version of this paper. The author would like to express his thanks to Mr. Kazushige Terui for his careful reading of the earlier draft and for his valuable comments. The author also would like to express his thanks to Drs. Jean-Yves Girard, Max Kanovitch, and Andre Scedrov for stimulating discussions and encouragements during the preparation of this paper.

本文言語English
ページ(範囲)154
ページ数1
ジャーナルElectronic Notes in Theoretical Computer Science
3
C
DOI
出版ステータスPublished - 1996

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs (Extended Abstract)」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル