dons' suggestion, which I heartily second, is somewhat aimed at practical type theory: http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/pl

dons' suggestion, which I heartily second, is somewhat aimed at practical type theory: http://www.cs.cmu.edu/~rwh/plbook/book.pdf http://www.cs.cmu.edu/~rwh/plbook/book.pdf Harper's thesis is that type theory is the backbone for language design. When you read his book you see him elaborate this and show how it applies to understanding and designing practical languages that work right.