> A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
And later on:
> A type system can be regarded as calculating a kind of static approximation to the runtime behaviors of the terms in a program. ... Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked," but the usage is standard.
The definitions you're using are the ones that he identifies as "arguably misnomers" but "standard". That is, they're fine as colloquial definitions but they are not the ones used in academic works. Academically speaking, a type system is a method of statically approximating the behavior of a computer program in order to rule out certain classes of behavior. Dynamic checks do not count.
As I've said elsewhere, I don't have a problem with people using the colloquial definitions. I do have a problem with people actively correcting someone who's using the more correct academic definitions. We should have both sets in our lexicons and be understanding when someone uses one versus the other.