基本信息
- 作者： [美]罗伯特·哈珀(Robert Harper)
- 译者： 张昱 胡明哲 中国科学技术大学等
- 丛书名： 计算机科学丛书
- 出版社：机械工业出版社
- ISBN：9787111697404
- 上架时间：2022-3-15
- 出版日期：2022 年3月
- 开本：16开
- 页码：399
- 版次：1-1
- 所属分类：计算机 > 计算机科学理论与基础知识 > 基础知识 > 综合
编辑推荐
CMU教授力作，全新视角阐释语言构造，未来编程语言设计者必读经典
内容简介
作译者
[美]罗伯特·哈珀(Robert Harper) 著：---作者简介---
罗伯特·哈珀(Robert Harper) 卡内基·梅隆大学计算机科学系教授，他的主要研究兴趣是类型论在编程语言的设计与实现中的应用，以及其元理论的机械化。Harper是Allen Newell卓越研究奖章和Herbert A. Simon卓越教学奖的获得者，并且是ACM会士。
---译者简介---
张昱 博士，中国科学技术大学计算机科学与技术学院、网络空间安全学院副教授。研究兴趣包括程序设计语言、操作系统和并行计算等，特别是面向人工智能和量子计算等新领域的编程系统、软件分析、异构计算与系统优化等。
胡明哲 中国科学技术大学网络空间安全学院博士研究生。主要研究方向为多语言软件的程序分析。
罗伯特·哈珀(Robert Harper) 卡内基·梅隆大学计算机科学系教授，他的主要研究兴趣是类型论在编程语言的设计与实现中的应用，以及其元理论的机械化。Harper是Allen Newell卓越研究奖章和Herbert A. Simon卓越教学奖的获得者，并且是ACM会士。
---译者简介---
张昱 博士，中国科学技术大学计算机科学与技术学院、网络空间安全学院副教授。研究兴趣包括程序设计语言、操作系统和并行计算等，特别是面向人工智能和量子计算等新领域的编程系统、软件分析、异构计算与系统优化等。
胡明哲 中国科学技术大学网络空间安全学院博士研究生。主要研究方向为多语言软件的程序分析。
目录
译者序
第2版前言
第1版前言
第一部分 判断和规则
第1章 抽象语法 2
1.1 抽象语法树 2
1.2 抽象绑定树 4
1.3 注记 8
习题 8
第2章 归纳定义 10
2.1 判断 10
2.2 推理规则 10
2.3 推导 11
2.4 规则归纳 13
2.5 迭代归纳定义和联立归纳定义 14
2.6 用规则定义函数 15
2.7 注记 15
习题 16
第3章 假言判断与一般性判断 17
3.1 假言判断 17
第2版前言
第1版前言
第一部分 判断和规则
第1章 抽象语法 2
1.1 抽象语法树 2
1.2 抽象绑定树 4
1.3 注记 8
习题 8
第2章 归纳定义 10
2.1 判断 10
2.2 推理规则 10
2.3 推导 11
2.4 规则归纳 13
2.5 迭代归纳定义和联立归纳定义 14
2.6 用规则定义函数 15
2.7 注记 15
习题 16
第3章 假言判断与一般性判断 17
3.1 假言判断 17
前言
就像构建软件系统的第2版会有风险一样，为教材编写第2版也会带来风险：很难在避免过度修改和不破坏原有基础的情况下做出实质性改进。为了避免“第二系统效应”，我试图通过更正、修订、扩展和删除来提高内容的一致性，删除一些偏离主题的话题，增加一些第1版中遗漏的话题，并为每一章引入习题。
此次修订删除了许多印刷错误，纠正了一些重大错误（特别是并行抽象机和Algol并发性的公式），并改进了全书的表述。一些章节被删除（一般模式匹配和极化、多态的受限形式），一些章节被完全重写（关于高阶种类的章节），一些章节被大幅修改（一般的和参数化归纳定义、并发和分布式 Algol），一些章节被重组（以更好地区分部分类型论和完全类型论），另外还新增了一章（关于类型细化）。本次修订删除了一些章节中对资料来源的不清晰引用，以避免混淆这些话题当前和原有的表述。全书引入了一套新的(可发音的）语言名称系统。习题试图扩展正文中的思想，而其解答往往涉及值得研究的重要技术思想。在课后作业中，尽量不包含按部就班的常规练习。
撰写本书的目的是建立一个全面阐述和分析编程语言中各种思想的框架。语言设计和编程方法要从手工制作发展到严密的学科，首先必须要有正确的定义。只有这样，才能进行有意义的分析和整合。我希望能帮助建立这样的基础。
感谢Stephen Brookes、Evan Cavallo、Karl Crary、Jon Sterling、James R. Wilcox和Todd Wilson对本版书稿的评审，并感谢他们提出的修订建议。感谢我的系主任Frank Pfenning对我完成本版工作的支持。还要感谢编辑Ada Brunstein和Lauren Cowles的指导和协助,感谢Andrew Shulaev对书稿的修正。
无论是作者还是出版商都无法保证本书中的定义、定理和证明没有错误，或者符合任何特定的适销性标准，或者满足任何特定应用的要求。使用本书的人员不应依赖它们来解决可能因不正确的解决方案而招致人身伤害或财产损失的问题。如果你执意按这种方式使用本书，后果自负。作者和出版商不承担因此造成的任何直接或间接损失。
Robert Harper
匹兹堡
2015年7月
此次修订删除了许多印刷错误，纠正了一些重大错误（特别是并行抽象机和Algol并发性的公式），并改进了全书的表述。一些章节被删除（一般模式匹配和极化、多态的受限形式），一些章节被完全重写（关于高阶种类的章节），一些章节被大幅修改（一般的和参数化归纳定义、并发和分布式 Algol），一些章节被重组（以更好地区分部分类型论和完全类型论），另外还新增了一章（关于类型细化）。本次修订删除了一些章节中对资料来源的不清晰引用，以避免混淆这些话题当前和原有的表述。全书引入了一套新的(可发音的）语言名称系统。习题试图扩展正文中的思想，而其解答往往涉及值得研究的重要技术思想。在课后作业中，尽量不包含按部就班的常规练习。
撰写本书的目的是建立一个全面阐述和分析编程语言中各种思想的框架。语言设计和编程方法要从手工制作发展到严密的学科，首先必须要有正确的定义。只有这样，才能进行有意义的分析和整合。我希望能帮助建立这样的基础。
感谢Stephen Brookes、Evan Cavallo、Karl Crary、Jon Sterling、James R. Wilcox和Todd Wilson对本版书稿的评审，并感谢他们提出的修订建议。感谢我的系主任Frank Pfenning对我完成本版工作的支持。还要感谢编辑Ada Brunstein和Lauren Cowles的指导和协助,感谢Andrew Shulaev对书稿的修正。
无论是作者还是出版商都无法保证本书中的定义、定理和证明没有错误，或者符合任何特定的适销性标准，或者满足任何特定应用的要求。使用本书的人员不应依赖它们来解决可能因不正确的解决方案而招致人身伤害或财产损失的问题。如果你执意按这种方式使用本书，后果自负。作者和出版商不承担因此造成的任何直接或间接损失。
Robert Harper
匹兹堡
2015年7月
媒体评论
本书是关于计算基础理论的综合读本。作者谈到了语言设计中出现的一系列令人惊讶的概念：从简单类型到多态性，从依赖类型到模块，从严格到懒惰到并行计算，从关于可扩展性行为的推理的证明技术到存在垃圾回收情况下的实用组合成本模型。更重要的是，整本书使用类型和类型理论的原理来组织章节，帮助我们发现正交的、可组合的抽象，这些抽象不仅自然地出现在编程语言的设计中，而且自然地出现在逻辑和数学中。这种方法有助于揭示隐藏在当今编程语言内部的基本结构，并为未来的设计提供了一种原则性的方法。
—— Greg Morrisett，康奈尔大学计算与信息科学学院院长
本书从数学上一个简单的框架和组织原则开始，将类型系统作为中心，揭示了编程语言这门兼具广度和优雅性的科学学科所蕴含的理论。作者丰富的经验和精辟的观点使得本书必将成为经典。
—— Andrew Pitts，剑桥大学理论计算机科学教授
本书对编程语言概念的讲解非常到位，全书架构统一，解释细致，使用的技术在分析和实现编程语言的实践中非常有用。本书作者是编程语言类型理论领域杰出的研究人员，本书正是作者多年教学经验的结晶。
—— Lars Birkedal，哥本哈根信息技术大学计算机科学教授
作者简介
罗伯特·哈珀（Robert Harper） 卡内基·梅隆大学计算机科学系教授，他的主要研究兴趣是类型论在编程语言的设计与实现中的应用，以及其元理论的机械化。Harper是Allen Newell卓越研究奖章和Herbert A. Simon卓越教学奖的获得者，并且是ACM会士。
译者简介
张昱 博士，中国科学技术大学计算机科学与技术学院、网络空间安全学院副教授。研究兴趣包括程序设计语言、操作系统和并行计算等，特别是面向人工智能和量子计算等新领域的编程系统、软件分析、异构计算与系统优化等。
胡明哲中国科学技术大学网络空间安全学院博士研究生。主要研究方向为多语言软件的程序分析。
—— Greg Morrisett，康奈尔大学计算与信息科学学院院长
本书从数学上一个简单的框架和组织原则开始，将类型系统作为中心，揭示了编程语言这门兼具广度和优雅性的科学学科所蕴含的理论。作者丰富的经验和精辟的观点使得本书必将成为经典。
—— Andrew Pitts，剑桥大学理论计算机科学教授
本书对编程语言概念的讲解非常到位，全书架构统一，解释细致，使用的技术在分析和实现编程语言的实践中非常有用。本书作者是编程语言类型理论领域杰出的研究人员，本书正是作者多年教学经验的结晶。
—— Lars Birkedal，哥本哈根信息技术大学计算机科学教授
作者简介
罗伯特·哈珀（Robert Harper） 卡内基·梅隆大学计算机科学系教授，他的主要研究兴趣是类型论在编程语言的设计与实现中的应用，以及其元理论的机械化。Harper是Allen Newell卓越研究奖章和Herbert A. Simon卓越教学奖的获得者，并且是ACM会士。
译者简介
张昱 博士，中国科学技术大学计算机科学与技术学院、网络空间安全学院副教授。研究兴趣包括程序设计语言、操作系统和并行计算等，特别是面向人工智能和量子计算等新领域的编程系统、软件分析、异构计算与系统优化等。
胡明哲中国科学技术大学网络空间安全学院博士研究生。主要研究方向为多语言软件的程序分析。
