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/12/1
Y1 - 2007/12/1
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
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 167
EP - 181
BT - Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday
A2 - Comon-Lundh, Hubert
A2 - Kirchner, Claude
A2 - Kirchner, Helene
ER -