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

Mitsuhiro Okada, Ryo Takemura

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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 languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages167-181
Number of pages15
Volume4600 LNCS
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4600 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Fingerprint

Calculi
Semantics
Completeness
Calculus
Demonstrations
Fragment
Term
Theorem
Intuitionistic Logic
Normal Form
Assignment
Logic
Imply
Direction compound
Framework

ASJC Scopus subject areas

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

Cite this

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). (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.

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4600 LNCS, pp. 167-181.
Okada M, Takemura R. 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. 2007. p. 167-181. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Okada, Mitsuhiro ; Takemura, Ryo. / Remarks on semantic completeness for proof-terms with Laird's dual affine/intuitionistic λ-calculus. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4600 LNCS 2007. pp. 167-181 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{3956ea07e19d4511af9f096026c63717,
title = "Remarks on semantic completeness for proof-terms with Laird's dual affine/intuitionistic λ-calculus",
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].",
author = "Mitsuhiro Okada and Ryo Takemura",
year = "2007",
language = "English",
isbn = "9783540731467",
volume = "4600 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "167--181",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

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 -