類型和程序設計語言

第1章  引論
 1.1  計算機科學中的類型
 1.2  類型系統(tǒng)的優(yōu)點
 1.3  類型系統(tǒng)和語言設計
 1.4  歷史概要
 1.5  相關閱讀
 第2章  數學基礎
 2.1  集合. 關系和函數
 2.2  有序集合
 2.3  序列
 2.4  歸納
 2.5  背景知識閱讀
 第一部分  無類型系統(tǒng)
 第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章  規(guī)范化
 12.1  簡單類型的規(guī)范化
 12.2  注釋
 第13章  引用
 13.1  引言
 13.2  類型化
 13.3  求值
 13.4  存儲類型
 13.5  安全性
 13.6  注釋
 第14章  異常
 14.1  提升異常
 14.2  處理異常
 14.3  帶值的異常
 第三部分  子 類 型 化
 第15章  子類型
 15.1  包含
 15.2  子類型關系
 15.3  子類型化和類型化的性質
 15.4  Top類型和Bottom類型
 15.5  子類型化及其他特征
 15. 6  子類型化的強制語義
 15.7  交叉類型和聯(lián)合類型
 15.8  注釋
 第16章  子類型的元理論
 16.1  算法子類型化
 16.2  算法類型化
 16.3  合類型和交類型
 16.4  算法類型化和Bottom類型
 第17章  子類型化的ML語言實現
 17.1  語法
 17.2  子類型化
 17.3  類型化
 第18章  實例分析:命令式對象
 18.1  什么是面向對象編程
 18.2  對象
 18.3  對象生成器
 18.4  子類型化
 18.5  聚集實例變量
 18.6  簡單類
 18.7  添加實例變量
 18.8  調用超類方法
 18.9  含self類
 18.10使用self的開放遞歸
 18.11開放遞歸及求值順序
 18.12更高效的實現
 18.13小結
 18.14注釋
 第19章  實例分析:輕量級的Java
 19.1  引言
 19.2  概要
 19.3  規(guī)范化和結構化的類型系統(tǒng)
 19.4  定義
 19.5  性質
 19.6  編碼及初始對象
 19.7  注釋
 第四部分  遞 歸 類 型
 第20章  遞歸類型簡介
 20.1  實例
 20.2  形式
 20.3  子類型化
 20.4  注釋
 第21章  遞歸類型元理論
 21.1  歸納和共歸納
 21.2  有限類型和無窮類型
 21.3  子類型
 21.4  傳遞性的偏離
 21.5  成員檢查
 21.6  更高效算法
 21.7  正則樹
 21.8  μ類型
 21.9  計算子表達式
 21.10關于指數級算法的閑話
 21.11子類型化同構遞歸類型
 21.12注釋第五部分  多    態(tài)
 第22章  類型重構
 22.1  類型變量和代換
 22.2  類型變量的兩個觀點
 22.3  基于約束的類型化
 22.4  合一
 22.5  主類型
 22.6  隱含的類型注釋
 22.7  let多態(tài)
 22.8  注釋
 第23章  全稱類型
 23.1  動機
 23.2  各種多態(tài)
 23.3  系統(tǒng)F
 23.4  實例
 23.5  基本性質
 23.6  抹除,可類型化,類型重構
 23.7  抹除和求值順序
 23.8  系統(tǒng)F片斷
 23.9  參數性
 23.10不可預言性
 23.11注釋
 第24章  存在類型
 24.1  引言
 24.2  帶存在量詞的數據抽象
 24.3  存在量詞編碼
 24.4  注釋
 第25章  系統(tǒng)F的ML實現
 25.1  類型的無名表示
 25.2  類型移位和代換
 25.3  項
 25.4  求值
 25.5  類型化
 第26章  囿量詞
 26.1  引言
 26.2  定義
 26.3  實例
 26.4  安全
 26.5  囿存在量詞類型
 26.6  注釋
 第27章  實例分析:命令性對象,約式
 第28章  囿量詞的元理論
 28.1  揭示
 28.2  最小化類型
 28.3  核心F<∶系統(tǒng)的子類型化
 28.4  全F<∶系統(tǒng)中的子類型化
 28.5  全F<∶系統(tǒng)的不可判定性
 28.6  合類型和交類型
 28.7  囿存在量詞
 28.8  囿量詞和最小類型
 第六部分  高 階 系 統(tǒng)
 第29章  類型算子和分類
 29.1  直覺
 29.2  定義
 第30章  高階多態(tài)
 30.1  定義
 30.2  實例
 30.3  性質
 30.4  Fω系統(tǒng)片斷
 30.5  進一步討論:依賴類型
 第31章  高階子類型化
 31.1  直覺
 31.2  定義
 31.3  性質
 31.4  注釋
 第32章  實例學習:純函數對象
 32.1  簡單對象
 32.2  子類型化
 32.3  囿量詞
 32.4  接口類型
 32.5  向對象發(fā)送消息
 32.6  簡單的類
 32.7  多態(tài)更新
 32.8  添加實例變量
 32.9  含self的類
 32.10注釋
 附錄A  部分習題解答
 附錄B  標記約定
 參考文獻
</font>