### 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 language | English |
---|---|

Pages (from-to) | 333-396 |

Number of pages | 64 |

Journal | Theoretical Computer Science |

Volume | 227 |

Issue number | 1-2 |

Publication status | Published - 1999 Sep 28 |

### Fingerprint

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

Research output: Contribution to journal › Article

*Theoretical Computer Science*, vol. 227, no. 1-2, pp. 333-396.

}

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 -