第1章 引言
1.1 基本概念
1.1.1 程序設(shè)計(jì)語(yǔ)言的建模
1.1.2 λ表示法
1.1.3 符號(hào)和約定
1.2 等式、歸約和語(yǔ)義
1.2.1 公理語(yǔ)義
1.2.2 操作語(yǔ)義
1.2.3 指稱語(yǔ)義
1.3 類型和類型系統(tǒng)
1.3.1 類型和類型系統(tǒng)
1.3.2 類型化語(yǔ)言的優(yōu)點(diǎn)
1.4 歸納法
1.4.1 表達(dá)式上的歸納
1.4.2 證明上的歸納
1.4.3 良基歸納
習(xí)題

第2章 泛代數(shù)和代數(shù)數(shù)據(jù)類型
2.1 引言
2.2 代數(shù)、基調(diào)和項(xiàng)
2.2.1 代數(shù)
2.2.2 代數(shù)項(xiàng)的語(yǔ)法
2.2.3 代數(shù)以及項(xiàng)在代數(shù)中的解釋
2.2.4 代換引理
2.3 等式、可靠性和完備性
2.3.1 等式
2.3.2 項(xiàng)代數(shù)
2.3.3 語(yǔ)義蘊(yùn)涵和等式證明系統(tǒng)
2.3.4 完備性的形式
2.3.5 同余、商和演繹完備性
2.3.6 非空類別和最小模型完備性
2.4 同態(tài)和初始性
2.4.1 同態(tài)和同構(gòu)
2.4.2 初始代數(shù)
2.5 代數(shù)數(shù)據(jù)類型
2.5.1 代數(shù)數(shù)據(jù)類型
2.5.2 初始代數(shù)語(yǔ)義和數(shù)據(jù)類型歸納
2.5.3 解釋沒有意義的項(xiàng)
2.5.4 錯(cuò)誤值的其他解決方法
2.6 重寫系統(tǒng)
2.6.1 基本定義
2.6.2 合流性和可證的相等性
2.6.3 終止性
2.6.4 臨界對(duì)
2.6.5 左線性無(wú)重疊重寫系統(tǒng)
2.6.6 局部合流、終止和合流之間的聯(lián)系
2.6.7 代數(shù)數(shù)據(jù)類型的應(yīng)用
習(xí)題

第3章 簡(jiǎn)單類型化λ演算
3.1 引言
3.2 類型和項(xiàng)
3.2.1 類型的語(yǔ)法
3.2.2 上下文有關(guān)語(yǔ)法
3.2.3 λ→項(xiàng)的語(yǔ)法
3，2.4 帶積、和及其他類型的項(xiàng)
3.2.5 定型算法
3.3 證明系統(tǒng)
3.3.1 等式和理論
3.3.2 歸約規(guī)則
3.3.3 有其他規(guī)則的歸約
3.4 通用模型、可靠性和完備性
3.4.1 通用模型和項(xiàng)的含義
3.4.2 應(yīng)用結(jié)構(gòu)、外延性和框架
3.4.3 環(huán)境條件
3.4.4 類型可靠性和等式可靠性
3.4.5 沒有空類型的完備性
3.4.6 有空類型的完備性
3.4.7 其他類型的通用模型
3.5 可計(jì)算函數(shù)編程語(yǔ)言
3.5.1 概述
3.5.2 PCF的語(yǔ)法
3.5.3 聲明和語(yǔ)法美化
3.5.4 程序和結(jié)果
3.5.5 公理語(yǔ)義
3.5.6 操作語(yǔ)義
3.5.7 由各種形式的語(yǔ)義定義的等價(jià)關(guān)系
3.5.8 記錄和n元組
3.6 各種歸約策略
3.6.1 歸約策略
3.6.2 最左歸約和惰性歸約
3.6.3 并行歸約
3.6.4 急切歸約
習(xí)題

第4章 類型化λ演算的模型
4.1 引言
4.2 遞歸函數(shù)和不動(dòng)點(diǎn)算子
4.2.1 遞歸函數(shù)和不動(dòng)點(diǎn)算子
4.2.2 有不動(dòng)點(diǎn)算子的急切歸約
4.2.3 PCF語(yǔ)言的編程實(shí)例
4.3 論域理論模型和不動(dòng)點(diǎn)
4.3.1 遞歸定義和不動(dòng)點(diǎn)算子
4.3.2 完全偏序集合、提升和笛卡兒積
4.3.3 連續(xù)函數(shù)
4.3.4 不動(dòng)點(diǎn)和完備連續(xù)層級(jí)
4.3.5 PCF的CPO模型
4.4 不動(dòng)點(diǎn)歸納
習(xí)題

第5章 命令式程序的語(yǔ)義
5.1 引言
5.2 Kernel語(yǔ)言
5.2.1 存儲(chǔ)單元
5.2.2 表達(dá)式的解釋
5.2.3 程序狀態(tài)
5.3 操作語(yǔ)義
5.3.1 表達(dá)式的求值
5.3.2 命令的執(zhí)行
5.4 指稱語(yǔ)義
5.4.1 帶狀態(tài)的類型化λ演算
5.4.2 語(yǔ)義函數(shù)
5.4.3 操作語(yǔ)義和指稱語(yǔ)義的等價(jià)
5.5 Kernel語(yǔ)言的Hoare邏輯
5.5.1 一階斷言
5.5.2 證明規(guī)則
5.5.3 可靠性
5.5.4 小結(jié)
習(xí)題

第6章 遞歸類型
6.1 引言
6.2 歸納和余歸納
6.2.1 余歸納現(xiàn)象
6.2.2 歸納和余歸納指南
6.2.3 代數(shù)和余代數(shù)
6.3 遞歸類型
6.3.1 遞歸類型總覽
6.3.2 遞歸的數(shù)據(jù)結(jié)構(gòu)
6.4 歸納類型和余歸納類型
6.4.1 歸納類型和余歸納類型總覽
6.4.2 幫助理解的實(shí)例
習(xí)題

第7章 多態(tài)性
7.1 引言
7.1.1 概述
7.1.2 類型作為函數(shù)變?cè)?br>7.2 直謂式多態(tài)演算
7.2.1 類型和項(xiàng)的語(yǔ)法
7.2.2 和其他形式多態(tài)性的比較
7.2.3 等式證明和歸約
7.2.4 ML風(fēng)格的多態(tài)聲明
7.3 非直謂式多態(tài)演算
7.3.1 引言
7.3.2 非直謂式多態(tài)λ演算的表達(dá)力
7.3.3 歸約的終止性
7.4 數(shù)據(jù)抽象和存在類型
7.5 類型表達(dá)式的分類
7.5.1 類型表達(dá)式的種類
7.5.2 類型表達(dá)式的定類與相等
7.5.3 項(xiàng)的定型
習(xí)題

第8章 依賴類型
8.1 引言
8.2 帶依賴類型的演算
8.2.1 依賴積類型
8.2.2 依賴和類型
8.3 帶依賴類型的程序設(shè)計(jì)
8.3.1 簡(jiǎn)化DML的實(shí)例
8.3.2 簡(jiǎn)化DML的定義
8.4 廣義積與廣義和
8.4.1 廣義積與廣義和概念
8.4.2 帶廣義積與廣義和的直謂式演算
8.4.3 ML模塊語(yǔ)言
8.4.4 用積與和來(lái)表示模塊
8.4.5 直謂性以及兩個(gè)全域之間的聯(lián)系
習(xí)題

第9章 命題和類型
9.1 引言
9.2 構(gòu)造邏輯
9.2.1 構(gòu)造語(yǔ)義
9.2.2 構(gòu)造邏輯
9.2.3 命題當(dāng)作類型
9.3 經(jīng)典邏輯
9.3.1 經(jīng)典邏輯和構(gòu)造邏輯的區(qū)別與聯(lián)系
9.3.2 經(jīng)典邏輯的規(guī)則
9.3.3 推導(dǎo)消去形式
9.3.4 證明的動(dòng)態(tài)性
習(xí)題

第10章 子定型
10.1 引言
10.2 有子定型的簡(jiǎn)單類型化λ演算
10.3 記錄
10.3.1 記錄子定型的一般性質(zhì)
10.3.2 帶記錄和子定型的類型化演算
10.4 子定型的語(yǔ)義模型
10.4.1 概述
10.4.2 子定型的轉(zhuǎn)換解釋
10.4.3 類型的子集解釋
10.5 對(duì)象的遞歸記錄模型
10.5.1 遞歸記錄類型
10.5.2 遞歸類型的子定型
習(xí)題

第11章 類型推斷
11.1 引言
11.2 帶類型變量的λ→類型推斷
11.2.1 語(yǔ)言λt→
11.2.2 代換、實(shí)例與合一
11.2.3 主定型算法
11.2.4 隱式定型
11.2.5 定型和合一的等價(jià)
11.3 帶多態(tài)聲明的類型推斷
11.3.1 ML類型推斷和多態(tài)變量
11.3.2 兩組隱式定型規(guī)則
11.3.3 類型推斷算法
習(xí)題
參考文獻(xiàn)