具體描述
類型理論在程序設計語言的發展中起著舉足輕重的作用，成熟的類型係統可以幫助完善程序設計本身，幫助運行係統檢查程序中的語義錯誤。
要理解類型係統在程序設計語言中發揮的作用，本書將是首選讀物。本書內容覆蓋基本操作語義及其相關證明技巧、無類型lambda演算、簡單類型係統、全稱多態和存在多態、類型重構、子類型化、囿界量詞、遞歸類型、類型算子等內容。本書既注重內容的廣度，也注重內容的深度，實用性強。在引入語言的語法對象時先舉例，然後給齣形式定義及基本證明，在對理論的進一步研究後給齣瞭類型檢查算法，並對每種算法都給齣瞭OCaml程序的具體實現。本書對類型理論中的概念都有詳細的闡述，為讀者提供瞭一個進一步理論學習的基礎。本書內容廣泛，讀者可以根據自己的需要有選擇地深入閱讀。
本書適閤從事程序設計的研究人員和開發人員，以及程序設計語言和類型理論的研究人員閱讀。可作為計算機專業高年級學生、研究生的學習教材。
著者簡介
圖書目錄
1.1 計算機科學中的類型
1.2 類型係統的優點
1.3 類型係統和語言設計
1.4 曆史概要
1.5 相關閱讀
第2章 數學基礎
2.1 集閤、關係和函數
2.2 有序集閤
2.3 序列
2.4 歸納
2.5 背景知識閱讀
第一部分 無類型係統
第3章 無類型算術錶達式
3.1 導論
3.2 語法
3.3 對項的歸納
3.4 語義形式
3.5 求值
3.6 注釋
第4章 算術錶達式的一個ML實現
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實現
7.1 項和上下文
7.2 移位和代換
7.3 求值
7.4 注釋
第二部分 簡 單 類 型
第8章 類型算術錶達式
8.1 類型
8.2 類型關係
8.3 安全性=進展+保持
第9章 簡單類型的lambda演算
9.1 函數類型
9.2 類型關係
9.3 類型的性質
9.4 Curry-Howard對應
9.5 抹除和類型性
9.6 Curry形式和Church形式
9.7 注釋
第10章 簡單類型的ML實現
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章 規範化
12.1 簡單類型的規範化
12.2 注釋
第13章 引用
13.1 引言
13.2 類型化
13.3 求值
13.4 存儲類型
13.5 安全性
13.6 注釋
第14章 異常
14.1 提升異常
14.2 處理異常
14.3 帶值的異常
第三部分 子類型化
第四部分 遞歸類型
附錄A 部分習題解答
附錄B 標記約定
參考文獻
· · · · · · (收起)
讀後感
原书写的很好读. 可惜翻译的很差. 拗口, 没有索引, 生僻的单词翻译的时候没有附上原英文单词. 总的来说, 翻译的很不认真.
評分原书写的很好读. 可惜翻译的很差. 拗口, 没有索引, 生僻的单词翻译的时候没有附上原英文单词. 总的来说, 翻译的很不认真.
評分原书写的很好读. 可惜翻译的很差. 拗口, 没有索引, 生僻的单词翻译的时候没有附上原英文单词. 总的来说, 翻译的很不认真.
評分原书写的很好读. 可惜翻译的很差. 拗口, 没有索引, 生僻的单词翻译的时候没有附上原英文单词. 总的来说, 翻译的很不认真.
評分原书写的很好读. 可惜翻译的很差. 拗口, 没有索引, 生僻的单词翻译的时候没有附上原英文单词. 总的来说, 翻译的很不认真.
用戶評價
隻看懂瞭中間兩章 也許搞定瞭behavioral subtyping再去看會恍然大悟
评分感覺自己水平未達到，讀起來吃力。翻譯也挺有問題的。
评分翻譯的很糟糕
评分翻譯的很糟糕
评分教授說值得一個字一個字讀的神書。 水平太差，暫時沒有看齣所以然來。看的中文版。 肯定是我的問題，因為每次聽教授講課都是 臥槽，還有這種操作 的感覺。 改天再看看英文版吧。
相關圖書
本站所有內容均為互聯網搜索引擎提供的公開搜索信息，本站不存儲任何數據與內容，任何內容與數據均與本站無關，如有需要請聯繫相關搜索引擎包括但不限於百度，google,bing,sogou 等
© 2025 book.quotespace.org All Rights Reserved. 小美書屋 版权所有