Normal proofs and their grammar

M. Takahashi, Y. Akama, Sachio Hirokawa

研究成果: 著書/レポートタイプへの貢献会議での発言

4 引用 (Scopus)

抄録

First we give a grammatical (or equational) description of the set {M normal form │ Γ ⊢ M : A} for a given basis Γ and a given type A in the simple type system, and give some applications of the description. Then we extend the idea to systems in λ-cube and more generally to normalizing pure type systems. The attempt resulted in derived (or ‘macro’) rules the totality of which is sound and complete for type assignments of normal terms. A feature of the derived rules is that they reflect the syntactic structure of legal terms in normal form, and thus they may give us more global view than the original definition of the systems.

元の言語英語
ホスト出版物のタイトルTheoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings
編集者John C. Mitchell, Masami Hagiya
出版者Springer Verlag
ページ465-493
ページ数29
ISBN(印刷物)9783540578871
出版物ステータス出版済み - 1 1 1994
イベント2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994 - Sendai, 日本
継続期間: 4 19 19944 22 1994

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
789 LNCS
ISSN(印刷物)0302-9743
ISSN(電子版)1611-3349

その他

その他2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994
日本
Sendai
期間4/19/944/22/94

Fingerprint

Syntactics
Type Systems
Grammar
Normal Form
Macros
Acoustic waves
Term
Regular hexahedron
Assignment
Syntax
Sound

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

これを引用

Takahashi, M., Akama, Y., & Hirokawa, S. (1994). Normal proofs and their grammar. : J. C. Mitchell, & M. Hagiya (版), Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings (pp. 465-493). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 789 LNCS). Springer Verlag.

Normal proofs and their grammar. / Takahashi, M.; Akama, Y.; Hirokawa, Sachio.

Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings. 版 / John C. Mitchell; Masami Hagiya. Springer Verlag, 1994. p. 465-493 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻 789 LNCS).

研究成果: 著書/レポートタイプへの貢献会議での発言

Takahashi, M, Akama, Y & Hirokawa, S 1994, Normal proofs and their grammar. : JC Mitchell & M Hagiya (版), Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 巻. 789 LNCS, Springer Verlag, pp. 465-493, 2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994, Sendai, 日本, 4/19/94.
Takahashi M, Akama Y, Hirokawa S. Normal proofs and their grammar. : Mitchell JC, Hagiya M, 編集者, Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings. Springer Verlag. 1994. p. 465-493. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Takahashi, M. ; Akama, Y. ; Hirokawa, Sachio. / Normal proofs and their grammar. Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings. 編集者 / John C. Mitchell ; Masami Hagiya. Springer Verlag, 1994. pp. 465-493 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5e5e8fb123204e398b1ade8c56bf4dcb,
title = "Normal proofs and their grammar",
abstract = "First we give a grammatical (or equational) description of the set {M normal form │ Γ ⊢ M : A} for a given basis Γ and a given type A in the simple type system, and give some applications of the description. Then we extend the idea to systems in λ-cube and more generally to normalizing pure type systems. The attempt resulted in derived (or ‘macro’) rules the totality of which is sound and complete for type assignments of normal terms. A feature of the derived rules is that they reflect the syntactic structure of legal terms in normal form, and thus they may give us more global view than the original definition of the systems.",
author = "M. Takahashi and Y. Akama and Sachio Hirokawa",
year = "1994",
month = "1",
day = "1",
language = "English",
isbn = "9783540578871",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "465--493",
editor = "Mitchell, {John C.} and Masami Hagiya",
booktitle = "Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Normal proofs and their grammar

AU - Takahashi, M.

AU - Akama, Y.

AU - Hirokawa, Sachio

PY - 1994/1/1

Y1 - 1994/1/1

N2 - First we give a grammatical (or equational) description of the set {M normal form │ Γ ⊢ M : A} for a given basis Γ and a given type A in the simple type system, and give some applications of the description. Then we extend the idea to systems in λ-cube and more generally to normalizing pure type systems. The attempt resulted in derived (or ‘macro’) rules the totality of which is sound and complete for type assignments of normal terms. A feature of the derived rules is that they reflect the syntactic structure of legal terms in normal form, and thus they may give us more global view than the original definition of the systems.

AB - First we give a grammatical (or equational) description of the set {M normal form │ Γ ⊢ M : A} for a given basis Γ and a given type A in the simple type system, and give some applications of the description. Then we extend the idea to systems in λ-cube and more generally to normalizing pure type systems. The attempt resulted in derived (or ‘macro’) rules the totality of which is sound and complete for type assignments of normal terms. A feature of the derived rules is that they reflect the syntactic structure of legal terms in normal form, and thus they may give us more global view than the original definition of the systems.

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

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

M3 - Conference contribution

AN - SCOPUS:21344495885

SN - 9783540578871

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

SP - 465

EP - 493

BT - Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings

A2 - Mitchell, John C.

A2 - Hagiya, Masami

PB - Springer Verlag

ER -