### Abstract

The purpose of this note is to give a demonstration of the completeness theorem of type assignment system for λ-terms of [Hindley 83] and [Coquand 05] with two directions of slight extensions. Firstly, using the idea of [Okada 96], [Okada-Terui 99] and [Hermant-Okada 07], we extend their completeness theorem to a stronger form which implies a normal form theorem. Secondly, we extend the simple type (the implicational fragment of intuitionistic logic) framework of [Hindley 83] and [Coquand 05] to a linear (affine) types (the {-o, &, →;}-fragment of affine logic) framework of [Laird 03, 05].

Original language | English |
---|---|

Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Pages | 167-181 |

Number of pages | 15 |

Volume | 4600 LNCS |

Publication status | Published - 2007 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 4600 LNCS |

ISSN (Print) | 03029743 |

ISSN (Electronic) | 16113349 |

### Fingerprint

### ASJC Scopus subject areas

- Computer Science(all)
- Biochemistry, Genetics and Molecular Biology(all)
- Theoretical Computer Science

### Cite this

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*(Vol. 4600 LNCS, pp. 167-181). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4600 LNCS).

**Remarks on semantic completeness for proof-terms with Laird's dual affine/intuitionistic λ-calculus.** / Okada, Mitsuhiro; Takemura, Ryo.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).*vol. 4600 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4600 LNCS, pp. 167-181.

}

TY - GEN

T1 - Remarks on semantic completeness for proof-terms with Laird's dual affine/intuitionistic λ-calculus

AU - Okada, Mitsuhiro

AU - Takemura, Ryo

PY - 2007

Y1 - 2007

N2 - The purpose of this note is to give a demonstration of the completeness theorem of type assignment system for λ-terms of [Hindley 83] and [Coquand 05] with two directions of slight extensions. Firstly, using the idea of [Okada 96], [Okada-Terui 99] and [Hermant-Okada 07], we extend their completeness theorem to a stronger form which implies a normal form theorem. Secondly, we extend the simple type (the implicational fragment of intuitionistic logic) framework of [Hindley 83] and [Coquand 05] to a linear (affine) types (the {-o, &, →;}-fragment of affine logic) framework of [Laird 03, 05].

AB - The purpose of this note is to give a demonstration of the completeness theorem of type assignment system for λ-terms of [Hindley 83] and [Coquand 05] with two directions of slight extensions. Firstly, using the idea of [Okada 96], [Okada-Terui 99] and [Hermant-Okada 07], we extend their completeness theorem to a stronger form which implies a normal form theorem. Secondly, we extend the simple type (the implicational fragment of intuitionistic logic) framework of [Hindley 83] and [Coquand 05] to a linear (affine) types (the {-o, &, →;}-fragment of affine logic) framework of [Laird 03, 05].

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

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

M3 - Conference contribution

AN - SCOPUS:38149033062

SN - 9783540731467

VL - 4600 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 167

EP - 181

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -