The standard text book would be Benjamin Pierce, "Types and Programming Languages".
Technically, soundness is a property of a type system. Sometimes we also say informally that a type would be (un)sound for a given term, in the sense that the underlyung type system would be (un)sound if it allowed assigning this type.
Nowadays, type soundness is typically proved syntactically, as the combination of two properties: Preservation (every computation step maintains types) and Progress (a well-typed non-terminated program can always take another step). Both of these properties are proved by standard induction proofs over the reduction relation and the typing relation of the language, respectively, with the help of some auxiliary lemmas. Pierce's book explains this in much detail.
There also is the stronger notion of semantic type soundness, that additionally ensures that, e.g. abstraction cannot be broken. But that generally is much more difficult to prove and subject of ongoing research.