@article{Joachimski:2003aa,
    Abstract = {Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed {$\lambda$}-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style {\`a}la Tait and Girard. It is also shown that the extension of the system with permutative conversions by η-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of ``immediate simplification''. By introducing an infinitely branching inductive rule the method even extends to G{\"o}del's T.},
    Author = {Joachimski, Felix and Matthes, Ralph},
    File = {Short proofs of normalization for the simplytyped A-calculus, permutative conversions and Godel's T - Joachimski-Matthes2003\_Article\_ShortProofsOfNormalizationForT - a - n.pdf},
    ISBN = {1432-0665},
    Journal = {Archive for Mathematical Logic},
    Number = {1},
    Pages = {59--87},
    Title = {Short proofs of normalization for the simply- typed {$\lambda$}-calculus, permutative conversions and G{\"o}del's T},
    URL = {https://doi.org/10.1007/s00153-002-0156-9},
    Volume = {42},
    Year = {2003},
    bdsk-url-1 = {https://doi.org/10.1007/s00153-002-0156-9},
    da = {2003/01/01},
    date-added = {2020-09-09 20:24:03 +0200},
    date-modified = {2020-09-09 20:24:03 +0200},
    id = {Joachimski2003},
    ty = {JOUR},
    doi = {10.1007/s00153-002-0156-9}
}

@article{Joachimski:2003aa, Abstract = {Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed {$\lambda$}-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style {`a}la Tait and Girard. It is also shown that the extension of the system with permutative conversions by η-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of ``immediate simplification''. By introducing an infinitely branching inductive rule the method even extends to G{\"o}del's T.}, Author = {Joachimski, Felix and Matthes, Ralph}, File = {Short proofs of normalization for the simplytyped A-calculus, permutative conversions and Godel's T - Joachimski-Matthes2003_Article_ShortProofsOfNormalizationForT - a - n.pdf}, ISBN = {1432-0665}, Journal = {Archive for Mathematical Logic}, Number = {1}, Pages = {59--87}, Title = {Short proofs of normalization for the simply- typed {$\lambda$}-calculus, permutative conversions and G{\"o}del's T}, URL = {https://doi.org/10.1007/s00153-002-0156-9}, Volume = {42}, Year = {2003}, bdsk-url-1 = {https://doi.org/10.1007/s00153-002-0156-9}, da = {2003/01/01}, date-added = {2020-09-09 20:24:03 +0200}, date-modified = {2020-09-09 20:24:03 +0200}, id = {Joachimski2003}, ty = {JOUR}, doi = {10.1007/s00153-002-0156-9} }