類型和程序設(shè)計(jì)語(yǔ)言

第1章  引論
 1.1  計(jì)算機(jī)科學(xué)中的類型
 1.2  類型系統(tǒng)的優(yōu)點(diǎn)
 1.3  類型系統(tǒng)和語(yǔ)言設(shè)計(jì)
 1.4  歷史概要
 1.5  相關(guān)閱讀
 第2章  數(shù)學(xué)基礎(chǔ)
 2.1  集合. 關(guān)系和函數(shù)
 2.2  有序集合
 2.3  序列
 2.4  歸納
 2.5  背景知識(shí)閱讀
 第一部分  無(wú)類型系統(tǒng)
 第3章  無(wú)類型算術(shù)表達(dá)式
 3.1  導(dǎo)論
 3.2  語(yǔ)法
 3.3  對(duì)項(xiàng)的歸納
 3.4  語(yǔ)義形式
 3.5  求值
 3.6  注釋
 第4章  算術(shù)表達(dá)式的一個(gè)ML實(shí)現(xiàn)
 4.1  語(yǔ)法
 4.2  求值
 4.3  其余部分
 第5章  無(wú)類型lambda演算
 5.1  基礎(chǔ)
 5.2  lambda演算中的程序設(shè)計(jì)
 5.3  形式性
 5.4  注釋
 第6章  項(xiàng)的無(wú)名稱表示
 6.1  項(xiàng)和上下文
 6.2  移位和代換
 6.3  求值
 第7章  lambda演算的一個(gè)ML實(shí)現(xiàn)
 7.1  項(xiàng)和上下文
 7.2  移位和代換
 7.3  求值
 7.4  注釋
 第二部分  簡(jiǎn) 單 類 型
 第8章  類型算術(shù)表達(dá)式
 8.1  類型
 8.2  類型關(guān)系
 8.3  安全性=進(jìn)展+保持
 第9章  簡(jiǎn)單類型的lambda演算
 9.1  函數(shù)類型
 9.2  類型關(guān)系
 9.3  類型的性質(zhì)
 9.4  CurryHoward對(duì)應(yīng)
 9.5  抹除和類型性
 9.6  Curry形式和Church形式
 9.7  注釋
 第10章  簡(jiǎn)單類型的ML實(shí)現(xiàn)
 10.1  上下文
 10.2  項(xiàng)和類型
 10.3  類型檢查
 第11章  簡(jiǎn)單擴(kuò)展
 11.1  基本類型
 11.2  單位類型
 11.3  導(dǎo)出形式:序列和通配符
 11.4  歸屬
 11.5  let綁定
 11.6  序?qū)?br /> 11.7  元組
 11.8  記錄
 11.9  和
 11.10變式
 11.11一般遞歸
 11.12列表
 第12章  規(guī)范化
 12.1  簡(jiǎn)單類型的規(guī)范化
 12.2  注釋
 第13章  引用
 13.1  引言
 13.2  類型化
 13.3  求值
 13.4  存儲(chǔ)類型
 13.5  安全性
 13.6  注釋
 第14章  異常
 14.1  提升異常
 14.2  處理異常
 14.3  帶值的異常
 第三部分  子 類 型 化
 第15章  子類型
 15.1  包含
 15.2  子類型關(guān)系
 15.3  子類型化和類型化的性質(zhì)
 15.4  Top類型和Bottom類型
 15.5  子類型化及其他特征
 15. 6  子類型化的強(qiáng)制語(yǔ)義
 15.7  交叉類型和聯(lián)合類型
 15.8  注釋
 第16章  子類型的元理論
 16.1  算法子類型化
 16.2  算法類型化
 16.3  合類型和交類型
 16.4  算法類型化和Bottom類型
 第17章  子類型化的ML語(yǔ)言實(shí)現(xiàn)
 17.1  語(yǔ)法
 17.2  子類型化
 17.3  類型化
 第18章  實(shí)例分析:命令式對(duì)象
 18.1  什么是面向?qū)ο缶幊?br /> 18.2  對(duì)象
 18.3  對(duì)象生成器
 18.4  子類型化
 18.5  聚集實(shí)例變量
 18.6  簡(jiǎn)單類
 18.7  添加實(shí)例變量
 18.8  調(diào)用超類方法
 18.9  含self類
 18.10使用self的開放遞歸
 18.11開放遞歸及求值順序
 18.12更高效的實(shí)現(xiàn)
 18.13小結(jié)
 18.14注釋
 第19章  實(shí)例分析:輕量級(jí)的Java
 19.1  引言
 19.2  概要
 19.3  規(guī)范化和結(jié)構(gòu)化的類型系統(tǒng)
 19.4  定義
 19.5  性質(zhì)
 19.6  編碼及初始對(duì)象
 19.7  注釋
 第四部分  遞 歸 類 型
 第20章  遞歸類型簡(jiǎn)介
 20.1  實(shí)例
 20.2  形式
 20.3  子類型化
 20.4  注釋
 第21章  遞歸類型元理論
 21.1  歸納和共歸納
 21.2  有限類型和無(wú)窮類型
 21.3  子類型
 21.4  傳遞性的偏離
 21.5  成員檢查
 21.6  更高效算法
 21.7  正則樹
 21.8  μ類型
 21.9  計(jì)算子表達(dá)式
 21.10關(guān)于指數(shù)級(jí)算法的閑話
 21.11子類型化同構(gòu)遞歸類型
 21.12注釋第五部分  多    態(tài)
 第22章  類型重構(gòu)
 22.1  類型變量和代換
 22.2  類型變量的兩個(gè)觀點(diǎn)
 22.3  基于約束的類型化
 22.4  合一
 22.5  主類型
 22.6  隱含的類型注釋
 22.7  let多態(tài)
 22.8  注釋
 第23章  全稱類型
 23.1  動(dòng)機(jī)
 23.2  各種多態(tài)
 23.3  系統(tǒng)F
 23.4  實(shí)例
 23.5  基本性質(zhì)
 23.6  抹除,可類型化,類型重構(gòu)
 23.7  抹除和求值順序
 23.8  系統(tǒng)F片斷
 23.9  參數(shù)性
 23.10不可預(yù)言性
 23.11注釋
 第24章  存在類型
 24.1  引言
 24.2  帶存在量詞的數(shù)據(jù)抽象
 24.3  存在量詞編碼
 24.4  注釋
 第25章  系統(tǒng)F的ML實(shí)現(xiàn)
 25.1  類型的無(wú)名表示
 25.2  類型移位和代換
 25.3  項(xiàng)
 25.4  求值
 25.5  類型化
 第26章  囿量詞
 26.1  引言
 26.2  定義
 26.3  實(shí)例
 26.4  安全
 26.5  囿存在量詞類型
 26.6  注釋
 第27章  實(shí)例分析:命令性對(duì)象,約式
 第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  實(shí)例
 30.3  性質(zhì)
 30.4  Fω系統(tǒng)片斷
 30.5  進(jìn)一步討論:依賴類型
 第31章  高階子類型化
 31.1  直覺
 31.2  定義
 31.3  性質(zhì)
 31.4  注釋
 第32章  實(shí)例學(xué)習(xí):純函數(shù)對(duì)象
 32.1  簡(jiǎn)單對(duì)象
 32.2  子類型化
 32.3  囿量詞
 32.4  接口類型
 32.5  向?qū)ο蟀l(fā)送消息
 32.6  簡(jiǎn)單的類
 32.7  多態(tài)更新
 32.8  添加實(shí)例變量
 32.9  含self的類
 32.10注釋
 附錄A  部分習(xí)題解答
 附錄B  標(biāo)記約定
 參考文獻(xiàn)
</font>