出版社: Cambridge University Press
出版年: 201644
页数: 512
定价: USD 80.74
装帧: Hardcover
ISBN: 9781107150300
内容简介 · · · · · ·
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.
作者简介 · · · · · ·
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.
喜欢读"Practical Foundations for Programming Languages"的人也喜欢 · · · · · ·
> 更多短评 4 条
Practical Foundations for Programming Languages的话题 · · · · · · ( 全部 条 )
Practical Foundations for Programming Languages的书评 · · · · · · ( 全部 0 条 )
读书笔记 · · · · · ·
我来写笔记
悟道洞穴人 (运用之妙，存乎一心)
Traditionally, languages are biased towards either eager or lazy evaluation. Eager lan guages use a byvalue dynamics for function applications, and evaluate the components of data structures when they are created. Lazy languages adopt the opposite strategy, pre ferring a byname dynamics for functions, and a lazy dynamics for data structures. The overhead of laziness is reduced by managing s...20170508 10:12

悟道洞穴人 (运用之妙，存乎一心)
These (memoization and splay tree) are examples of benign storage effects, uses of mutation in a data structure to improve efficiency without disrupting its functional behavior. One class of examples are selfadjusting data structures that reorganize themselves during one use to improve efficiency of later uses. Another class of examples are memoized, or lazy, data structures. Benign effects su...20170508 09:57

悟道洞穴人 (运用之妙，存乎一心)
Modernized Algol introduces the concept of block structurce, i.e. the scope of assignables. the stacklike behavior of assignables is a characteristic feature of what are known as Algollike languages. the language (Modernized Algol) maintains a sharp distinction between variables and assignables. variables are introduced by lambdaabstraction and given meaning by substitution. Assignables are ...20170508 09:06

悟道洞穴人 (运用之妙，存乎一心)
implicit parallesim theorem declares that the results from sequential structural dynamics and parallel structural dynamics concide. That's why you can develop parallel program on a sequential platform and then run it on a parallel platform and still get the correct result. For this reason, this theorem is also called deterministic parallelism theorem. On the other hand, cocurrency has the conce...20170508 03:34
implicit parallesim theorem declares that the results from sequential structural dynamics and parallel structural dynamics concide. That's why you can develop parallel program on a sequential platform and then run it on a parallel platform and still get the correct result. For this reason, this theorem is also called deterministic parallelism theorem. On the other hand, cocurrency has the concept of threadsafe which implies nondeterministic results.
The thing is that the result of parallism is deterministic because of join and we don't have assignables, though the evaluation process is not. Concurrency is always nondeterministic because we have introduced assignables. Another way to interpret this is that
This is the root difference between parallism and concurrency, the result and the context instead of the execution.
回应 20170508 03:34

悟道洞穴人 (运用之妙，存乎一心)
Modernized Algol introduces the concept of block structurce, i.e. the scope of assignables. the stacklike behavior of assignables is a characteristic feature of what are known as Algollike languages. the language (Modernized Algol) maintains a sharp distinction between variables and assignables. variables are introduced by lambdaabstraction and given meaning by substitution. Assignables are ...20170508 09:06

悟道洞穴人 (运用之妙，存乎一心)
These (memoization and splay tree) are examples of benign storage effects, uses of mutation in a data structure to improve efficiency without disrupting its functional behavior. One class of examples are selfadjusting data structures that reorganize themselves during one use to improve efficiency of later uses. Another class of examples are memoized, or lazy, data structures. Benign effects su...20170508 09:57

悟道洞穴人 (运用之妙，存乎一心)
Traditionally, languages are biased towards either eager or lazy evaluation. Eager lan guages use a byvalue dynamics for function applications, and evaluate the components of data structures when they are created. Lazy languages adopt the opposite strategy, pre ferring a byname dynamics for functions, and a lazy dynamics for data structures. The overhead of laziness is reduced by managing s...20170508 10:12

悟道洞穴人 (运用之妙，存乎一心)
implicit parallesim theorem declares that the results from sequential structural dynamics and parallel structural dynamics concide. That's why you can develop parallel program on a sequential platform and then run it on a parallel platform and still get the correct result. For this reason, this theorem is also called deterministic parallelism theorem. On the other hand, cocurrency has the conce...20170508 03:34
implicit parallesim theorem declares that the results from sequential structural dynamics and parallel structural dynamics concide. That's why you can develop parallel program on a sequential platform and then run it on a parallel platform and still get the correct result. For this reason, this theorem is also called deterministic parallelism theorem. On the other hand, cocurrency has the concept of threadsafe which implies nondeterministic results.
The thing is that the result of parallism is deterministic because of join and we don't have assignables, though the evaluation process is not. Concurrency is always nondeterministic because we have introduced assignables. Another way to interpret this is that
This is the root difference between parallism and concurrency, the result and the context instead of the execution.
回应 20170508 03:34

悟道洞穴人 (运用之妙，存乎一心)
Traditionally, languages are biased towards either eager or lazy evaluation. Eager lan guages use a byvalue dynamics for function applications, and evaluate the components of data structures when they are created. Lazy languages adopt the opposite strategy, pre ferring a byname dynamics for functions, and a lazy dynamics for data structures. The overhead of laziness is reduced by managing s...20170508 10:12

悟道洞穴人 (运用之妙，存乎一心)
These (memoization and splay tree) are examples of benign storage effects, uses of mutation in a data structure to improve efficiency without disrupting its functional behavior. One class of examples are selfadjusting data structures that reorganize themselves during one use to improve efficiency of later uses. Another class of examples are memoized, or lazy, data structures. Benign effects su...20170508 09:57

悟道洞穴人 (运用之妙，存乎一心)
Modernized Algol introduces the concept of block structurce, i.e. the scope of assignables. the stacklike behavior of assignables is a characteristic feature of what are known as Algollike languages. the language (Modernized Algol) maintains a sharp distinction between variables and assignables. variables are introduced by lambdaabstraction and given meaning by substitution. Assignables are ...20170508 09:06

悟道洞穴人 (运用之妙，存乎一心)
implicit parallesim theorem declares that the results from sequential structural dynamics and parallel structural dynamics concide. That's why you can develop parallel program on a sequential platform and then run it on a parallel platform and still get the correct result. For this reason, this theorem is also called deterministic parallelism theorem. On the other hand, cocurrency has the conce...20170508 03:34
implicit parallesim theorem declares that the results from sequential structural dynamics and parallel structural dynamics concide. That's why you can develop parallel program on a sequential platform and then run it on a parallel platform and still get the correct result. For this reason, this theorem is also called deterministic parallelism theorem. On the other hand, cocurrency has the concept of threadsafe which implies nondeterministic results.
The thing is that the result of parallism is deterministic because of join and we don't have assignables, though the evaluation process is not. Concurrency is always nondeterministic because we have introduced assignables. Another way to interpret this is that
This is the root difference between parallism and concurrency, the result and the context instead of the execution.
回应 20170508 03:34
这本书的其他版本 · · · · · · ( 全部2 )

Cambridge University Press （2012）暂无评分 4人读过
以下豆列推荐 · · · · · · ( 全部 )
 hoho (123)
 Theoretical Computer Science (李卓华)
 计算机科学 (左元)
 Prog Lang Theory & Compiler Construction (𝕾𝖚𝖓)
 cs (破po)
谁读这本书?
二手市场
订阅关于Practical Foundations for Programming Languages的评论:
feed: rss 2.0
1 有用 梦里醉逍遥 20170220
Robert Harper 真是惜字如金的典范，能用数学公式表达出来的东西就绝不给你举例子……（其实这本书就读了一半，但容我假装一下）
1 有用 悟道洞穴人 20170508
没有废话，全程无尿点。偶尔讲个例子还都是 modularity, polymorphism, recursive type 这种不太直观，非讲不可的
0 有用 rockAfella 20170509
句句精辟，一针见血
1 有用 nomadmonad 20190803
非常硬核的pl入门(keng)书，这标题也是有点搞笑，书里的东西一点也不practical....太难了
1 有用 nomadmonad 20190803
非常硬核的pl入门(keng)书，这标题也是有点搞笑，书里的东西一点也不practical....太难了
0 有用 rockAfella 20170509
句句精辟，一针见血
1 有用 悟道洞穴人 20170508
没有废话，全程无尿点。偶尔讲个例子还都是 modularity, polymorphism, recursive type 这种不太直观，非讲不可的
1 有用 梦里醉逍遥 20170220
Robert Harper 真是惜字如金的典范，能用数学公式表达出来的东西就绝不给你举例子……（其实这本书就读了一半，但容我假装一下）