程序設計語言理論(第2版)（簡體書）

《程序設計語言理論(第2版)》給出分析程序設計語言語法性質、操作性質和語義性質的一個框架，該框架基於λ演算系統。全書主要圍繞著一系列的λ演算來組織，該系列中λ演算的類型系統依次變得越來越復雜，這些λ演算用來分析和討論相應的程序設計語言概念，如多態性、抽象數據類型、依賴類型、子定型等。以類型系統為中心對程序設計語言進行的這種研究，在軟件工程、語言設計、高性能編譯器、高可信軟件和形式程序驗證等方面有著重要應用。
《程序設計語言理論(第2版)》可作為高等院校計算機科學及相關專業的研究生教材，也可供計算機軟件工程高級技術人員參考。

第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 類型推斷算法
習題
參考文獻