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

Research output: Contribution to journalArticle

33 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
Publication statusPublished - 1999 Sep 28

Fingerprint

Higher-order Logic
Cut-elimination
Linear Logic
Normalization
Semantics
First-order
First-order Logic
Natural Extension
Monoid
Completeness
Phase Space

Keywords

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

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic. / Okada, Mitsuhiro.

In: Theoretical Computer Science, Vol. 227, No. 1-2, 28.09.1999, p. 333-396.

Research output: Contribution to journalArticle

@article{8c9f0897163a48bcb28e47e384532cd9,
title = "Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic",
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.",
keywords = "Cut-elimination, Higher-order logic, Linear logic, Normalization theorem, Phase semantics",
author = "Mitsuhiro Okada",
year = "1999",
month = "9",
day = "28",
language = "English",
volume = "227",
pages = "333--396",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-2",

}

TY - JOUR

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

AU - Okada, Mitsuhiro

PY - 1999/9/28

Y1 - 1999/9/28

N2 - 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.

AB - 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.

KW - Cut-elimination

KW - Higher-order logic

KW - Linear logic

KW - Normalization theorem

KW - Phase semantics

UR - http://www.scopus.com/inward/record.url?scp=0000610062&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0000610062&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0000610062

VL - 227

SP - 333

EP - 396

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -