Normal proofs and their grammar

M. Takahashi, Y. Akama, S. Hirokawa

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

    4 Citations (Scopus)

    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.

    Original languageEnglish
    Title of host publicationTheoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings
    EditorsMasami Hagiya, John C. Mitchell
    PublisherSpringer Verlag
    Pages465-493
    Number of pages29
    ISBN (Print)9783540578871
    DOIs
    Publication statusPublished - 1994
    Event2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994 - Sendai, Japan
    Duration: Apr 19 1994Apr 22 1994

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume789 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Other

    Other2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994
    CountryJapan
    CitySendai
    Period4/19/944/22/94

    All Science Journal Classification (ASJC) codes

    • Theoretical Computer Science
    • Computer Science(all)

    Fingerprint Dive into the research topics of 'Normal proofs and their grammar'. Together they form a unique fingerprint.

    Cite this