顶部
  1. 首页
  2. 图书产品
  3. 程序设计语言理论（第二版）
收藏

程序设计语言理论（第二版）

样章
作者：
陈意云 张昱
定价：
36.50元
ISBN：
978-7-04-028404-1
版面字数：
420.000千字
开本：
16开
全书页数：
351页
装帧形式：
平装
重点项目：
暂无
出版时间：
2010-02-08
读者对象：
高等教育
一级分类：
计算机/教育技术类
二级分类：
计算机类专业核心课程
三级分类：
程序设计基础

本书给出分析程序设计语言语法性质、操作性质和语义性质的一个框架，该框架基于λ演算系统。全书主要围绕着一系列的λ演算来组织，该系列中λ演算的类型系统依次变得越来越复杂，这些λ演算用来分析和讨论相应的程序设计语言概念，如多态性、抽象数据类型、依赖类型、子定型等。以类型系统为中心对程序设计语言进行的这种研究，在软件工程、语言设计、高性能编译器、高可信软件和形式程序验证等方面有着重要应用。

本书可作为高等院校计算机科学及相关专业的研究生教材，也可供计算机软件工程高级技术人员参考。

  • 第1章 引言
    • 1.1 基本概念
      • 1.1.1 程序设计语言的建模
      • 1.1.2 λ表示法
      • 1.1.3 符号和约定
    • 1.2 等式、归约和语义
      • 1.2.1 公理语义
      • 1.2.2 操作语义
      • 1.2.3 指称语义
    • 1.3 类型和类型系统
      • 1.3.1 类型和类型系统
      • 1.3.2 类型化语言的优点
    • 1.4 归纳法
      • 1.4.1 表达式上的归纳
      • 1.4.2 证明上的归纳
      • 1.4.3 良基归纳
    • 习题
  • 第2章 泛代数和代数数据类型
    • 2.1 引言
    • 2.2 代数、基调和项
      • 2.2.1 代数
      • 2.2.2 代数项的语法
      • 2.2.3 代数以及项在代数中的解释
      • 2.2.4 代换引理
    • 2.3 等式、可靠性和完备性
      • 2.3.1 等式
      • 2.3.2 项代数
      • 2.3.3 语义蕴涵和等式证明系统
      • 2.3.4 完备性的形式
      • 2.3.5 同余、商和演绎完备性
      • 2.3.6 非空类别和最小模型完备性
    • 2.4 同态和初始性
      • 2.4.1 同态和同构
      • 2.4.2 初始代数
    • 2.5 代数数据类型
      • 2.5.1 代数数据类型
      • 2.5.2 初始代数语义和数据类型归纳
      • 2.5.3 解释没有意义的项
      • 2.5.4 错误值的其他解决方法
    • 2.6 重写系统
      • 2.6.1 基本定义
      • 2.6.2 合流性和可证的相等性
      • 2.6.3 终止性
      • 2.6.4 临界对
      • 2.6.5 左线性无重叠重写系统
      • 2.6.6 局部合流、终止和合流之间的联系
      • 2.6.7 代数数据类型的应用
    • 习题
  • 第3章 简单类型化λ演算
    • 3.1 引言
    • 3.2 类型和项
      • 3.2.1 类型的语法
      • 3.2.2 上下文有关语法
      • 3.2.3 λ→项的语法
      • 3.2.4 带积、和及其他类型的项
      • 3.2.5 定型算法
    • 3.3 证明系统
      • 3.3.1 等式和理论
      • 3.3.2 归约规则
      • 3.3.3 有其他规则的归约
    • 3.4 通用模型、可靠性和完备性
      • 3.4.1 通用模型和项的含义
      • 3.4.2 应用结构、外延性和框架
      • 3.4.3 环境条件
      • 3.4.4 类型可靠性和等式可靠性
      • 3.4.5 没有空类型的完备性
      • 3.4.6 有空类型的完备性
      • 3.4.7 其他类型的通用模型
    • 3.5 可计算函数编程语言
      • 3.5.1 概述
      • 3.5.2 PCF的语法
      • 3.5.3 声明和语法美化
      • 3.5.4 程序和结果
      • 3.5.5 公理语义
      • 3.5.6 操作语义
      • 3.5.7 由各种形式的语义定义的等价关系
      • 3.5.8 记录和n元组
    • 3.6 各种归约策略
      • 3.6.1 归约策略
      • 3.6.2 最左归约和惰性归约
      • 3.6.3 并行归约
      • 3.6.4 急切归约
    • 习题
  • 第4章 类型化λ演算的模型
    • 4.1 引言
    • 4.2 递归函数和不动点算子
      • 4.2.1 递归函数和不动点算子
      • 4.2.2 有不动点算子的急切归约
      • 4.2.3 PCF语言的编程实例
    • 4.3 论域理论模型和不动点
      • 4.3.1 递归定义和不动点算子
      • 4.3.2 完全偏序集合、提升和笛卡儿积
      • 4.3.3 连续函数
      • 4.3.4 不动点和完备连续层级
      • 4.3.5 PCF的CPO模型
    • 4.4 不动点归纳
    • 习题
  • 第5章 命令式程序的语义
    • 5.1 引言
    • 5.2 Kernel语言
      • 5.2.1 存储单元
      • 5.2.2 表达式的解释
      • 5.2.3 程序状态
    • 5.3 操作语义
      • 5.3.1 表达式的求值
      • 5.3.2 命令的执行
    • 5.4 指称语义
      • 5.4.1 带状态的类型化λ演算
      • 5.4.2 语义函数
      • 5.4.3 操作语义和指称语义的等价
    • 5.5 Kernel语言的Hoare逻辑
      • 5.5.1 一阶断言
      • 5.5.2 证明规则
      • 5.5.3 可靠性
      • 5.5.4 小结
    • 习题
  • 第6章 递归类型
    • 6.1 引言
    • 6.2 归纳和余归纳
      • 6.2.1 余归纳现象
      • 6.2.2 归纳和余归纳指南
      • 6.2.3 代数和余代数
    • 6.3 递归类型
      • 6.3.1 递归类型总览
      • 6.3.2 递归的数据结构
    • 6.4 归纳类型和余归纳类型
      • 6.4.1 归纳类型和余归纳类型总览
      • 6.4.2 帮助理解的实例
    • 习题
  • 第7章 多态性
    • 7.1 引言
      • 7.1.1 概述
      • 7.1.2 类型作为函数变元
    • 7.2 直谓式多态演算
      • 7.2.1 类型和项的语法
      • 7.2.2 和其他形式多态性的比较
      • 7.2.3 等式证明和归约
      • 7.2.4 ML风格的多态声明
    • 7.3 非直谓式多态演算
      • 7.3.1 引言
      • 7.3.2 非直谓式多态λ演算的表达力
      • 7.3.3 归约的终止性
    • 7.4 数据抽象和存在类型
    • 7.5 类型表达式的分类
      • 7.5.1 类型表达式的种类
      • 7.5.2 类型表达式的定类与相等
      • 7.5.3 项的定型
    • 习题
  • 第8章 依赖类型
    • 8.1 引言
    • 8.2 带依赖类型的演算
      • 8.2.1 依赖积类型
      • 8.2.2 依赖和类型
    • 8.3 带依赖类型的程序设计
      • 8.3.1 简化DML的实例
      • 8.3.2 简化DML的定义
    • 8.4 广义积与广义和
      • 8.4.1 广义积与广义和概念
      • 8.4.2 带广义积与广义和的直谓式演算
      • 8.4.3 ML模块语言
      • 8.4.4 用积与和来表示模块
      • 8.4.5 直谓性以及两个全域之间的联系
    • 习题
  • 第9章 命题和类型
    • 9.1 引言
    • 9.2 构造逻辑
      • 9.2.1 构造语义
      • 9.2.2 构造逻辑
      • 9.2.3 命题当作类型
    • 9.3 经典逻辑
      • 9.3.1 经典逻辑和构造逻辑的区别与联系
      • 9.3.2 经典逻辑的规则
      • 9.3.3 推导消去形式
      • 9.3.4 证明的动态性
    • 习题
  • 第10章 子定型
    • 10.1 引言
    • 10.2 有子定型的简单类型化λ演算
    • 10.3 记录
      • 10.3.1 记录子定型的一般性质
      • 10.3.2 带记录和子定型的类型化演算
    • 10.4 子定型的语义模型
      • 10.4.1 概述
      • 10.4.2 子定型的转换解释
      • 10.4.3 类型的子集解释
    • 10.5 对象的递归记录模型
      • 10.5.1 递归记录类型
      • 10.5.2 递归类型的子定型
    • 习题
  • 第11章 类型推断
    • 11.1 引言
    • 11.2 带类型变量的λ→类型推断
      • 11.2.1 语言t→λ
      • 11.2.2 代换、实例与合一
      • 11.2.3 主定型算法
      • 11.2.4 隐式定型
      • 11.2.5 定型和合一的等价
    • 11.3 带多态声明的类型推断
      • 11.3.1 ML类型推断和多态变量
      • 11.3.2 两组隐式定型规则
      • 11.3.3 类型推断算法
    • 习题
  • 参考文献

相关图书

C++: 面向对象程序设计

李涛

￥32.00 收藏

C++: 面向对象程序设计（第2版）

李涛 杨剑波

￥35.00 收藏

C++程序设计与问题求解（第6版 影印版）

Nell Dale， Chip Weems

￥90.00 收藏

C++程序设计（第三版 影印版）

Nell Dale Chip Weems

￥50.00 收藏

C/C++程序设计案例教程实验与实训指导

梅险等

￥25.20 收藏

C程序设计

张长海、陈娟

￥30.00 收藏

C语言程序设计(第3版)

苏小红 王宇颖 孙志岗 等

￥45.00 收藏

C语言程序设计(第4版)

苏小红 赵玲玲 孙志岗 王宇颖 等

￥49.00 收藏

C语言程序设计(第4版)

苏小红 赵玲玲 孙志岗 王宇颖 等

￥49.00 收藏

C语言程序设计学习指导(第2版)

苏小红 车万翔 王甜甜

￥30.60 收藏

C语言程序设计学习指导(第2版)

苏小红 车万翔 王甜甜

￥30.60 收藏

C语言程序设计学习指导(第3版)

苏小红 王甜甜 车万翔

￥37.50 收藏

C语言程序设计（第5版）

苏小红 张彦航 赵玲玲 李东 编著

￥59.00 收藏

JAVA与面向对象程序设计（影印版）

[美]Paul S. Wang

￥39.50 收藏

Java程序设计

许满武等

￥36.80 收藏