Normal proofs and their grammar

M. Takahashi, Y. Akama, S. Hirokawa

研究成果: Conference contribution

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.

本文言語English
ホスト出版物のタイトルTheoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings
編集者Masami Hagiya, John C. Mitchell
出版社Springer Verlag
ページ465-493
ページ数29
ISBN(印刷版)9783540578871
DOI
出版ステータスPublished - 1994
外部発表はい
イベント2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994 - Sendai, Japan
継続期間: 1994 4月 191994 4月 22

出版物シリーズ

名前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

Other

Other2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994
国/地域Japan
CitySendai
Period94/4/1994/4/22

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Normal proofs and their grammar」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル