類型和程序設(shè)計語言

內(nèi)容概要

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

書籍目錄

　第1章 引論　　1.1 計算機(jī)科學(xué)中的類型　　1.2 類型系統(tǒng)的優(yōu)點　　1.3 類型系統(tǒng)和語言設(shè)計　　1.4 歷史概要　　1.5 相關(guān)閱讀　第2章 數(shù)學(xué)基礎(chǔ)　　2.1 集合、關(guān)系和函數(shù)　　2.2 有序集合　　2.3 序列　　2.4 歸納　　2.5 背景知識閱讀第一部分 無類型系統(tǒng)　第3章 無類型算術(shù)表達(dá)式　　3.1 導(dǎo)論　　3.2 語法　　3.3 對項的歸納　　3.4 語義形式　　3.5 求值　　3.6 注釋　第4章 算術(shù)表達(dá)式的一個ML實現(xiàn)　　4.1 語法　　4.2 求值　　4.3 其余部分　第5章 無類型lambda演算　　5.1 基礎(chǔ)　　5.2 lambda演算中的程序設(shè)計　　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章 類型算術(shù)表達(dá)式　　8.1 類型　　8.2 類型關(guān)系　　8.3 安全性=進(jìn)展+保持　第9章 簡單類型的lambda演算　　9.1 函數(shù)類型　　9.2 類型關(guān)系　　9.3 類型的性質(zhì)　　9.4 Curry?Howard對應(yīng)　　9.5 抹除和類型性　　9.6 Curry形式和Church形式　　9.7 注釋　第10章 簡單類型的ML實現(xiàn)　　10.1 上下文　　10.2 項和類型　　10.3 類型檢查　第11章 簡單擴(kuò)展　　11.1 基本類型　　11.2 單位類型　　11.3 導(dǎo)出形式：序列和通配符　　11.4 歸屬　　11.5 let綁定　　11.6 序?qū)Α　?1.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 部分習(xí)題解答附錄B 標(biāo)記約定參考文獻(xiàn)

圖書封面

圖書標(biāo)簽Tags

無

評論、評分、閱讀與下載

---

    類型和程序設(shè)計語言 PDF格式下載

---