想得起来的几本书瞎扯一下：

## 侧重代码实现
Types and Programming Languages：从最简单的无类型 lambda calculus 讲到 System F，有 OCaml 代码示例和习题，难度适中。
Software Foundations：全程使用 Coq 代码进行讲解。习惯边看书边敲代码来实现的话推荐这本。
Essentials of Programming Languages：全程使用 Scheme 代码讲解，看完以后会写很多有趣的解释器。这本书是 Daniel Friedman 作品，他还有 The Little XX 系列，问答式的文风简直是写给小朋友看的，可能会有人喜欢。。

## 侧重数学理论
Type Theory and Formal Proof：讲的形式系统比 TAPL 更多（包含 dependent types ），侧重点不在于代码实现和为编程服务，而在于将 Type Theory 作为数学形式化的 building blocks。这书有中译本，不过建议看原文。。
Practical Foundations for Programming Languages：Robert Harper 的作品，比 TAPL 硬核许多，介绍的语言特性和形式系统比 TAPL 覆盖更为全面。看过其他教材以后不妨挑战一下这本。