In this innovative book, Professor Robert Harper offers a fresh perspective on the fundamentals of programming languages through the use of type theory. Whereas most textbooks on this subject emphasize taxonomy, Harper instead emphasizes genetics, examining the building blocks from which all programming languages are constructed. The result is an introduction to programming the...
In this innovative book, Professor Robert Harper offers a fresh perspective on the fundamentals of programming languages through the use of type theory. Whereas most textbooks on this subject emphasize taxonomy, Harper instead emphasizes genetics, examining the building blocks from which all programming languages are constructed. The result is an introduction to programming theory that is both accessible and practical.
作者简介
· · · · · ·
Robert Harper has been a member of the faculty of Computer Science at Carnegie Mellon University since 1988. His main research interest is in the application of type theory to the design and implementation of programming languages and to the development of systems for mechanization of mathematics. Professor Harper is a recipient of the Allen Newell Medal for Research Excellence...
Robert Harper has been a member of the faculty of Computer Science at Carnegie Mellon University since 1988. His main research interest is in the application of type theory to the design and implementation of programming languages and to the development of systems for mechanization of mathematics. Professor Harper is a recipient of the Allen Newell Medal for Research Excellence and the Herbert A. Simon Award for Teaching Excellence at Carnegie Mellon and is a Fellow of the Association for Computing Machinery.
the implicit parallelism theorem states that parallelism does not affect the semantics of a program, only the efficiency of its execution. Correctness is not affected by parallelism, only efficiency (查看原文)
the language (Modernized Algol) maintains a sharp distinction between variables and assignables. variables are introduced by lambda-abstraction and given meaning by substitution. Assignables are introduced by a declaration and are given meaning by mutation (assignment and retrivial of their contents). Expressions evaluate to values and have no effect on assignable. commnads are executed for their effect on assignables and return a value. composition of commands not only sequences their execution order, but also passes the value returned by the first to the second before it is executed (查看原文)
Ganzinger
Cambridge University Press2016版
0 有用 Duke 2020-10-21 23:40:30
补标，和TAPL定位差不多，这是第一版，第二版改写了不少
0 有用 sigsegv 2021-04-12 14:52:01
在CMU上课用的教材，书本身比较晦涩（很多bob夹带私货的术语/暴论），如果不是上过CMU的课的话很难理解。
0 有用 ダルクvan 2025-03-19 16:42:16 广东
对读者非常不友好的一本书：CMU 在教授这门的时候，重点就没放在过前面的这个 part one 上面，都是从 lambda calculus 开始讲起，一个 PFPL 的 supplement，那我说确实啊，lambda calculus 是很好的例子，很适合教授。 PFPL 只能通过 supplement 来挽尊。要我说 Harper 本不该将这个书出版，因为出版了之后基本不允许大的变动了，而... 对读者非常不友好的一本书：CMU 在教授这门的时候，重点就没放在过前面的这个 part one 上面，都是从 lambda calculus 开始讲起，一个 PFPL 的 supplement，那我说确实啊，lambda calculus 是很好的例子，很适合教授。 PFPL 只能通过 supplement 来挽尊。要我说 Harper 本不该将这个书出版，因为出版了之后基本不允许大的变动了，而这本书是需要变动的。而且 Harper 的符号用法实在是太特别了… (展开)