  This paper shows how a recently developed view of typing as small-step
abstract reduction, due to Kuan, MacQueen, and Findler, can be used to recast
the development of simple type theory from a rewriting perspective. We show how
standard meta-theoretic results can be proved in a completely new way, using
the rewriting view of simple typing. These meta-theoretic results include
standard type preservation and progress properties for simply typed lambda
calculus, as well as generalized versions where typing is taken to include both
abstract and concrete reduction. We show how automated analysis tools developed
in the term-rewriting community can be used to help automate the proofs for
this meta-theory. Finally, we show how to adapt a standard proof of
normalization of simply typed lambda calculus, for the rewriting approach to
typing.
