收藏
Types and Programming Languages - Benjamin C. Pierce

Types and Programming Languages

Benjamin C. Pierce

出版社

The MIT Press

出版时间

2002-02-01

ISBN

9780262162098

评分

★★★★★

标签

类型系统编程语言programming计算机科学

书籍介绍
A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems--and of programming languages from a type-theoretic perspective -- -has important applications in software engineering, language design, high-performance compilers, and security.This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material.The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages.
AI导读
核心看点
  • 系统介绍类型系统与编程语言基础理论
  • 结合编程实例，采用务实的操作视角
  • 涵盖从简单语言到子类型等高级特性
适合谁读
  • 计算机科学及编程语言专业学生
  • 对类型系统理论感兴趣的开发者
  • 从事编译器设计与语言研究的学者
读前提醒
  • 内容理论性强，需耐心阅读数学证明
  • 建议配合课程学习，认真完成课后练习
  • 中文译本质量一般，建议参考英文原版
读者共识
  • 公认的经典教材，内容严谨且全面
  • 难度较大，后半部分如递归类型极难
  • 不做证明难以真正理解，需反复研读

本导读基于书籍简介、目录、原文摘录、短评和书评生成，不等同于全文精读。

精彩摘录
  • "Q: Why bother doing proofs about programming languages? They are almost always boring if the definitions are right. A: The definitions are almost always wrong."
  • "n one end of the spec- trum are powerful frameworks such as Hoare logic, algebraic specification languages, modal logics, and denotational semantics. These can be used to express very general correctness properties but are often cumbersome to use and demand a good deal of sophistication on the part "
  • "At the other end are techniques of much more modest power—modest enough that automatic checkers can be built into compilers, linkers, or program analyzers"
  • "The more abstract focuses on connections between various “pure typed lambda-calculi” and varieties of logic, via the Curry-Howard correspondence"
  • "they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence,"
  • "type systems are also used to enforce higher-level modularity properties and to protect the in- tegrity of user-defined abstractions."
  • "Chains can be either finite or infinite, but we are more interested in infinite ones, as in the next definition"
  • "The mathemati- cal foundations of inductive reasoning will be considered in more detail in Chapter 21, where we will see that all these specific induction principles are instances of a single deeper idea."
用户评论
上TAPL的时候认认真真把这本书看了一遍，收获很多，而且课程拿了 A+开心～
跳过了各种证明 ...
书是挺好的，但是越来越读不懂了(2015/3-2015/7)
内容很全很丰富，还要多刷几次！
在皮尔斯荣膺 SIGPLAN 杰出教育奖之际，我终于把 TAPL 读完了。全书从 STLC 一直讲到了 F-omega-sub，中间还通过余归纳讲解了递归类型，基本上覆盖了依值类型之外的常见类型论，而且元理论上的性质几乎都附有纸笔证明。皮尔斯对 OOP 也是真爱，引入子类型之后有整整四章做对象建模的案例分析。
数理逻辑回炉重造 😔
PL的经典入门书，打开了新世界的大门
没啥好说的，pl必读书。从16年开始反反复复看了差不多有三年。后面几章有点难，而且难点不在如何理解concept，而在这些concept到底在讲了一个啥？或者说在整个system中起到了哪些关键性的不可替代性的作用。
得做proof啊！不做proof怎么可能懂 哭泣 STLC的strong normalization 书里一下就过去了 在不同的知识储备下看感觉是完全不一样的。。。
The MIT Press的其他书籍查看全部

收藏