內容簡介
λ演算的主要特色是對於函式和其他可計算的值的一種記法，以及一個等式邏輯和用於表達式求值的一組規則。
本書中最簡單的系統是稱為泛代數的一個等式系統，它可以用來公理化和分析通常用於程式設計的許多數據類型。更先進的技術機制，諸如邏輯關係的方法、範疇論和遞歸定義類型的語義在中間的幾章論述。本書最後三章研究多態類型，連帶討論了抽象數據類型的說明形式和程式模組、類型適應性和類型推理。
本書可作為理論計算機科學、軟體系統和數學專業的大學本科高年級或者研究生初始學習階段的教材，同時也適合用於高等研究的技術參考書。
圖書目錄
第1章 引言
1.1 模型程式設計語言
1.2 λ記法
1.3 等式，歸納和語義
1.4 類型和類型系統
1.5 記法和數學約定
1.6 集合論基礎知識
1.7 語法和語義
1.8 歸納法
第2章 PCF語言
2.1 引言
2.2 PCF語法
2.3 PCF程式及其語義
2.4 PCF歸納和符號解釋程式
2.5 PCF編程樣例，表達能和限度
2.6 PCF的變體和擴展
第3章 泛代數及代數數據類型
3.1 引言
3.2 代數規範概述
3.3 代數，基調和項
3.4 等式，可靠性和完備性
3.5 同態和始代數
3.6 代數數據類型
3.7 重寫系統
第4章 簡單類型化λ演算
4.1 引言
4.2 類型
4.3 項
4.4 證明系統
4.5 Henkin模型，可靠性和完備性
第5章 類型化λ演算模型
5.1 引言
5.2 域論模型和不動點
5.3 不動點歸納
5.4 計算適當性和完全抽象
5.5 遞歸理論模型
5.6 部分等價關係和遞歸
第6章 命令式程式
6.1 引言
6.2 while程式
6.3 操作語義
6.4 指稱語義
……
第7章 範疇和遞歸類型
第8章 邏輯關係
第9章 多態與模組性
第10章 類型適應性和相關概念
第11章 類型推理
參考文獻
