@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 {\textquoteleft}macro{\textquoteright}) 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 S. Hirokawa",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994 ; Conference date: 19-04-1994 Through 22-04-1994",
year = "1994",
doi = "10.1007/3-540-57887-0_111",
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 = "Masami Hagiya and Mitchell, {John C.}",
booktitle = "Theoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings",
address = "Germany",
}