類型和程序設計語言

內(nèi)容概要

類型理論在程序設計語言的發(fā)展中起著舉足輕重的作用，成熟的類型系統(tǒng)可以幫助完善程序設計本身，幫助運行系統(tǒng)檢查程序中的語義錯誤。   要理解類型系統(tǒng)在程序設計語言中發(fā)揮的作用，本書將是首選讀物。本書內(nèi)容覆蓋基本操作語義及其相關證明技巧、無類型lambda演算、簡單類型系統(tǒng)、全稱多態(tài)和存在多態(tài)、類型重構、子類型化、囿界量詞、遞歸類型、類型算子等內(nèi)容。本書既注重內(nèi)容的廣度，也注重內(nèi)容的深度，實用性強。在引入語言的語法對象時先舉例，然后給出形式定義及基本證明，在對理論的進一步研究后給出了類型檢查算法，并對每種算法都給出了OCaml程序的具體實現(xiàn)。本書對類型理論中的概念都有詳細的闡述，為讀者提供了一個進一步理論學習的基礎。本書內(nèi)容廣泛，讀者可以根據(jù)自己的需要有選擇地深入閱讀。   本書適合從事程序設計的研究人員和開發(fā)人員，以及程序設計語言和類型理論的研究人員閱讀。可作為計算機專業(yè)高年級學生、研究生的學習教材。

書籍目錄

　第1章 引論　　1.1 計算機科學中的類型　　1.2 類型系統(tǒng)的優(yōu)點　　1.3 類型系統(tǒng)和語言設計　　1.4 歷史概要　　1.5 相關閱讀　第2章 數(shù)學基礎　　2.1 集合、關系和函數(shù)　　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實現(xiàn)　　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實現(xiàn)　　7.1 項和上下文　　7.2 移位和代換　　7.3 求值　　7.4 注釋第二部分 簡 單 類 型　第8章 類型算術表達式　　8.1 類型　　8.2 類型關系　　8.3 安全性=進展+保持　第9章 簡單類型的lambda演算　　9.1 函數(shù)類型　　9.2 類型關系　　9.3 類型的性質　　9.4 Curry?Howard對應　　9.5 抹除和類型性　　9.6 Curry形式和Church形式　　9.7 注釋　第10章 簡單類型的ML實現(xiàn)　　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章 異?！　?4.1 提升異?！　?4.2 處理異常　　14.3 帶值的異常第三部分 子類型化第四部分 遞歸類型附錄A 部分習題解答附錄B 標記約定參考文獻

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

    類型和程序設計語言 PDF格式下載

---