Glynn Winskel, "The Formal Semantics of Programming Languages", 1993 -- a bit dated but still quite good. Covers basic semantics/type theory. Benjamin Pierce,

Glynn Winskel, "The Formal Semantics of Programming Languages", 1993 -- a bit dated but still quite good. Covers basic semantics/type theory. Benjamin Pierce, "Types and Programming Languages", 2002 -- y'know, just your basic type theory. Benjamin Pierce, "Advanced Topics in Types and Programming Languages", 2005 -- Chapter 10 is a juicy 128 pages on Hindley-Milner type inference. Good for both theory and implementation tricks. It looks at HM typing as a constraint system where the rules are Just Right so that if you get a solution you get a solution that is "maximally nice". It describes variants that are perhaps not quite as beautiful but which in some ways are "better" (= can statically check more of your code or where the programmer can express him or herself freer). If you want to know more about unification, which is how HM type inference and checking is usually/originally stated: Franz Baader and Wayne Snyder, "Handbook of Automated Reasoning", 2001 -- chapter 8 is called 'Unification theory'. Peter Norvig, "Correcting A[sic] Widespread Error in Unification Algorithms", 1991 -- many published algorithms were subtly wrong. Unification is really an example of a term rewriting system: Franz Baader and Tobias Nipkow, "Term Rewriting and All That", 1998. It is amazing how much there is to say about a 10-line algorithm (Algorithm W) / such a short set of typing rules / such a small constraint system as the HM type system.