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]. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Okada, M., & Takemura, R. (2007). Remarks on semantic completeness for proof-terms with Laird’s dual affine/intuitionistic λ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4600 LNCS, pp. 167–181). Springer Verlag. https://doi.org/10.1007/978-3-540-73147-4_8
Mendeley helps you to discover research relevant for your work.