Normal proofs and their grammar

M. Takahashi, Y. Akama, S. Hirokawa

    研究成果: Chapter in Book/Report/Conference proceedingConference 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.

    本文言語英語
    ホスト出版物のタイトルTheoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings
    編集者Masami Hagiya, John C. Mitchell
    出版社Springer Verlag
    ページ465-493
    ページ数29
    ISBN(印刷版)9783540578871
    DOI
    出版ステータス出版済み - 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
    Country日本
    CitySendai
    Period4/19/944/22/94

    All Science Journal Classification (ASJC) codes

    • Theoretical Computer Science
    • Computer Science(all)

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

    引用スタイル