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