### 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 | Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday |

Editors | Hubert Comon-Lundh, Claude Kirchner, Helene Kirchner |

Pages | 167-181 |

Number of pages | 15 |

Publication status | Published - 2007 Dec 1 |

### 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) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'Remarks on semantic completeness for proof-terms with Laird's dual affine/intuitionistic λ-calculus'. Together they form a unique fingerprint.

## Cite this

Okada, M., & Takemura, R. (2007). Remarks on semantic completeness for proof-terms with Laird's dual affine/intuitionistic λ-calculus. In H. Comon-Lundh, C. Kirchner, & H. Kirchner (Eds.),

*Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday*(pp. 167-181). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4600 LNCS).