类型和程序设计语言认领

类型理论在程序设计语言的发展中起着举足轻重的作用，成熟的类型系统可以帮助完善程序设计本身，帮助运行系统检查程序中的语义错误。 要理解类型系统在程序设计语言中发挥的作用，本书将是首选读物。本书内容覆盖基本操作语义及其相关证明技巧、无类型lambda演算、简单类型系统、全称多态和存在多态、类型重构、子类型化、囿界量词、递归类型、类型算子等内容。本书既注重内容的广度，也注重内容的深度，实用性... 更多