Martin-Lof類型論程序設計導論

1.引言
1.1　類型論用于程序設計
　1.2　構造數學
　1.3　類型論的不同表述系統(tǒng)
1.4　程序邏輯的實現
2.集合，命題和規(guī)格說明的等同
2.1　命題作為集合
　2.2　命題作為任務和程序的規(guī)格說明
3.表達式與定義相等性
3.1 作用
3.2　抽象
3.3　組合
3.4　選取
3.5　帶名分部的組合
　3.6　相關度
3.7　定義
　3.8　什么是具某個相關度的表達式的定義
　3.9　兩個表達式之間相等性的定義
第一部分　多型集合
　4.判斷形式的語義
　 4.1 范疇判斷
　 4.2　帶一個前提的假設判斷
　 4.3　帶多個前提的假設判斷
　5.一般規(guī)則
　 5.1　前提
　 5.2　命題作為集合
　5.3　相等性規(guī)則
　 5.4　集合規(guī)則
　 5.5　替代規(guī)則
　6.枚舉集合
　　6.1　永假與空集合
　 6.2　單元素集合與真命題
　 6.3　集合B001
　7.集合族的笛氏積
　 7.1　形式規(guī)則及其論證
　 7.2　另一種原始非典則形式
　 7.3 由Ⅱ集合定義的常元
　8.相等性集合
　8.1　內涵相等性
　 8.2　外延相等性
　 8.3　Ⅱ-集合元素的n相等性
　9.自然數
　10.列表
　11.兩個集合的笛氏積
　 11.1　形式規(guī)則
　 11.2 函數的外延相等性
　12.兩個集合的不交和
　13.集合族的不交和
　14.小集合之集合(第一全域)
　 14.1　形式規(guī)則
　 14.2　消去規(guī)則
　15.良序
　 15.1　用良序表示歸納定義集合
　16.一般樹
16.1　形式規(guī)則
16.2　與良序集合構造子的關系
16.3　樹集合構造子的異體
16.4　不同樹集合的例子
第二部分　子集合
　17.基本集合理論中的子集合
　18.子集合理論
　 18.1　無前提判斷
　18.2　假設判斷
　 18.3　子集合理論中的一般規(guī)則
　 18.4　子集合理論中的命題常元
　 18.5 由概括形成子集合
　 18.6　子集合理論中單獨的成集算子
　　18.7　帶全域的子集合
第三部分　單型集合
第四部分　例子
參考文獻
附錄A 常元及其相關度
附錄B　操作語義