This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics. Language concepts are precisely defined by their static and dynamic semantics, presenting the essential tools both intuitively and rigorously while relying on only elementary mathematics. These tools are used to analyze and prove properties of languages...
This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics. Language concepts are precisely defined by their static and dynamic semantics, presenting the essential tools both intuitively and rigorously while relying on only elementary mathematics. These tools are used to analyze and prove properties of languages and provide the framework for combining and comparing language features. The broad range of concepts includes fundamental data types such as sums and products, polymorphic and abstract types, dynamic typing, dynamic dispatch, subtyping and refinement types, symbols and dynamic classification, parallelism and cost semantics, and concurrency and distribution. The methods are directly applicable to language implementation, to the development of logics for reasoning about programs, and to the formal verification language properties such as type safety. This thoroughly revised second edition includes exercises at the end of nearly every chapter and a new chapter on type refinements.
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
2 有用 悟道洞穴人 2017-05-08 10:42:36
没有废话，全程无尿点。偶尔讲个例子还都是 modularity, polymorphism, recursive type 这种不太直观，非讲不可的
4 有用 梦里醉逍遥 2017-02-20 13:35:36
Robert Harper 真是惜字如金的典范，能用数学公式表达出来的东西就绝不给你举例子……（其实这本书就读了一半，但容我假装一下）
0 有用 Duke 2020-10-21 23:41:09
补标
0 有用 rock-A-fella 2017-05-09 10:21:34
句句精辟，一针见血
4 有用 nomadmonad 2019-08-03 21:50:11
非常硬核的pl入门(keng)书，这标题也是有点搞笑，书里的东西一点也不practical....太难了