类型和程序设计语言——国外计算机科学教材系列
|
读过这本书吗？
最近在读
读过
想读
还不熟悉
|
图书城书列：
加入到博客或社交网站：
|
|
我来评论这本书：
内容提要：
类型理论在程序设计语言的发展中起着举足轻重的作用，成熟的类型系统可以帮助完善程序设计本身，帮助运行系统检查程序中的语义错误。
要理解类型系统在程序设计语言中发挥的作用，本书将是首选读物。本书内容覆盖基本操作语义及其相关证明技巧、无类型lambda演算、简单类型系统、全称多态和存在多态、类型重构、子类型化、囿界量词、递归类型、类型算子等内容。本书既注重内容的广度，也注重内容的深度，实用性强。在引入语言的语法对象时先举例，然后给出形式定义及基本证明，在对理论的进一步研究后给出了类型检查算法，并对每种算法都给出了OCaml程序的具体实现。本书对类型理论中的概念都有详细的阐述，为读者提供了一个进一步理论学习的基础。本书内容广泛，读者可以根据自己的需要有选择地深入阅读。 本书适合从事程序设计的研究人员和开发人员，以及程序设计语言和类型理论的研究人员阅读。可作为计算机专业高年级学生、研究生的学习教材。 编辑推荐：
类型是计算机程序语言的酵母，若少了它，程序难以被计算机消化。这本优秀的图书集应用、理论和实现为一体，通过类型指引我们走进丰富的程序语言世界。本书的作者在应用、理论和实现方面有着丰富的经验。
——Robin Milner，剑桥大学计算机实验室 只在出色的学者能写出如此严谨、清晰的书籍，才能将理论与实现技术融为一体，才能体现出丰富的教学经验，才能算得上该领域的专家。 ——John Reynolds，卡内基·梅隆大学计算机学院 Pierce的书不介对程序语言中的类型进行了详细介绍，而且将理论和实践有机地结合起来，提供了一个成功的典范。未来许多年间，此书必将成为权威参考书目。 ——Robert Harper，卡内基·梅隆大学计算机系教授 本书是经过了对多个问题的仔细推敲、选择后写成的。它侧重于实用，同时也不缺乏必要的理论。书中的练习充分考虑了初级读者、高级读者、程序员和理论研究人员的不同需要。 ——Henk Barendregt，荷兰纳米根大学教学与计算机科学教师 目录：
第1章 引论
1.1 计算机科学中的类型 1.2 类型系统的优点 1.3 类型系统和语言设计 1.4 历史概要 1.5 相关阅读 第2章 数学基础 2.1 集合、关系和函数 2.2 有序集合 2.3 序列 2.4 归纳 2.5 背景知识阅读 第一部分 无类型系统 第3章 无类型算术表达式 3.1 导论 3.2 语法 3.3 对项的归纳 3.4 语义形式 3.5 求值 3.6 注释 第4章 算术表达式的一个ML实现 4.1 语法 4.2 求值 4.3 其余部分 第5章 无类型lambda演算 5.1 基础 5.2 lambda演算中的程序设计 5.3 形式性 5.4 注释 第6章 项的无名称表示 6.1 项和上下文 6.2 移位和代换 6.3 求值 第7章 lambda演算的一个ML实现 7.1 项和上下文 7.2 移位和代换 7.3 求值 7.4 注释 第二部分 简 单 类 型 第8章 类型算术表达式 8.1 类型 8.2 类型关系 8.3 安全性=进展+保持 第9章 简单类型的lambda演算 9.1 函数类型 9.2 类型关系 9.3 类型的性质 9.4 Curry?Howard对应 9.5 抹除和类型性 9.6 Curry形式和Church形式 9.7 注释 第10章 简单类型的ML实现 10.1 上下文 10.2 项和类型 10.3 类型检查 第11章 简单扩展 11.1 基本类型 11.2 单位类型 11.3 导出形式：序列和通配符 11.4 归属 11.5 let绑定 11.6 序对 11.7 元组 11.8 记录 11.9 和 11.10变式 11.11一般递归 11.12列表 第12章 规范化 12.1 简单类型的规范化 12.2 注释 第13章 引用 13.1 引言 13.2 类型化 13.3 求值 13.4 存储类型 13.5 安全性 13.6 注释 第14章 异常 14.1 提升异常 14.2 处理异常 14.3 带值的异常 第三部分 子类型化 第四部分 递归类型 附录A 部分习题解答 附录B 标记约定 参考文献 译者序：
类型系统的研究，以及从类型论的角度研究程序语言已经是一个充满活力的研究领域，主要应用于软件工程、语言设计、高性能编译器的实现和安全。本书以一种很容易理解的方式介绍这一领域所涉及的基本定义、理论结果（从基本lambda演算、类型理论和程序语言理论）和实现技术。
现代软件工程广泛地使用形式化方法，确保系统按照隐式或显式的说明方式运行。这方面出现过一些过于理论化的框架，如Hoare逻辑、代数说明语言、模态逻辑和指称语义等。由于这些理论实用性不强，尤其难以被程序员所接受，所以出现了一些实用的技术，如将自动检查器放到编译器、连接器或程序分析器中的技术。至今最流行、最完善的轻量级形式..
前言：
对类型系统的研究，以及从类型理论的角度研究程序语言已成为一种充满活力的领域，它们主要应用于软件工程、语言设计、高性能编译器的实现和安全。本书将对该领域的基本概念，研究成果及技术手段展开全面的阐述。
读者对象
本书针对两类读者：(1)从事程序语言和类型理论研究的研究生和研究人员；(2)希望了解程序语言理论中关键概念的计算机科学领域研究生和高年级本科生。对于前一类读者，本书覆盖了该领域的大部分内容，为读者深入研究提供了依据。对于后一类读者，提供了介绍性的材料和例子以及分析。本书既可以作为一般研究生水平的教材，也可以作为程序语言的高级研讨班的教材。
本书的目标
..
|