This paper introduces typed operational semantics, a class of formal systems which define a reduction to normal form for the welltyped terms of a particular type theory. These systems lead to a new approach to the metatheory for type theories, which we develop here for the simply typed lambda calculus. A similar approach can be used to study systems with dependent types.