Theoretical computer science self-study resources for programmers
There are several ways to learn about type theory. For a working programmer, 
   Types and Programming Languages by B. Pierce is a good start.
Practical Foundations for Programming Languages by R. Harper might also be good. If you want a bit of easy to read background on operational semantics, 
I recommend G. Winskel's, The Formal Semantics of Programming Languages: An Introduction. With T. Nipkow, G. Klein, Concrete Semantics, a variant of Winskel's book has been formalised for the Isabelle/HOL interactive proof assistant. I suspect it's really difficult to get to grips with a prover just from this (or any) book, you'd want an expert nearby to ask questions.
If you want a more mathematical approach to type-theory, you could look at
J. R. Hindley, J. P. Seldin, Lambda-Calculus and Combinators: An Introduction, or
H. Barendregt's, Lambda Calculi with Types. Although I wouldn't recommend starting from Barendregt.

If you want a single recommendation, I'd say read all of Pierce except Part VI (Higher-Order Systems), and implement the toy languages the book discusses. You'll end up with a strong grounding in type theory, and probably a better programmer too.