掃一掃
關注中圖網
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
實用編程語言理論基礎(原書第2版) 版權信息
- ISBN：9787111697404
- 條形碼：9787111697404 ; 978-7-111-69740-4
- 裝幀：一般膠版紙
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
實用編程語言理論基礎(原書第2版) 本書特色
CMU教授著作，講解基于類型系統和結構操作語義的實用方法，未來編程語言設計者必讀經典
實用編程語言理論基礎(原書第2版) 內容簡介
本書提出了一種基于類型系統和結構操作語義的編程語言理論。第2版經過全面修訂，幾乎每章都包含習題，并新增一章討論類型細化。本書涉及的概念廣泛，包括：基本數據類型，多態和抽象類型，動態定型，動態分派，子類型和類型細化，符號和動態分類，并行和成本語義，并發和分布。書中對不同編程語言的特性做了分析、證明和比較，所提供的方法可直接應用于語言的實現、程序推理邏輯的研發以及語言特性的形式化驗證，具有較高的實用性。本書不僅可以作為高等學校計算機相關專業的編程語言理論課程教材，也可供相關領域的科研人員和技術人員參考閱讀。
實用編程語言理論基礎(原書第2版) 目錄
譯者序
第2版前言
第1版前言
**部分 判斷和規則
第1章 抽象語法 2
1.1 抽象語法樹 2
1.2 抽象綁定樹 4
1.3 注記 8
習題 8
第2章 歸納定義 10
2.1 判斷 10
2.2 推理規則 10
2.3 推導 11
2.4 規則歸納 13
2.5 迭代歸納定義和聯立歸納定義 14
2.6 用規則定義函數 15
2.7 注記 15
習題 16
第3章 假言判斷與一般性判斷 17
3.1 假言判斷 17
3.1.1 可導性 17
3.1.2 可納性 18
3.2 假言歸納定義 20
3.3 一般性判斷 21
3.4 泛型歸納定義 22
3.5 注記 23
習題 23
第二部分 靜態語義和動態語義
第4章 靜態語義 28
4.1 語法 28
4.2 類型系統 29
4.3 結構性質 30
4.4 注記 31
習題 31
第5章 動態語義 33
5.1 轉換系統 33
5.2 結構化動態語義 34
5.3 上下文動態語義 36
5.4 等式動態語義 37
5.5 注記 39
習題 39
第6章 類型安全 40
6.1 保持性 40
6.2 進展性 41
6.3 運行時錯誤 42
6.4 注記 43
習題 43
第7章 求值動態語義 44
7.1 求值動態語義 44
7.2 結構化動態語義和求值動態語義
的關系 45
7.3 重溫類型安全 45
7.4 成本動態語義 46
7.5 注記 47
習題 47
第三部分 全函數
第8章 函數定義和值 50
8.1 一階函數 50
8.2 高階函數 51
8.3 求值動態語義和定義等同 53
8.4 動態作用域 54
8.5 注記 55
習題 55
第9章 高階遞歸的系統T 56
9.1 靜態語義 56
9.2 動態語義 57
9.3 可定義性 58
9.4 不可定義性 59
9.5 注記 61
習題 61
第四部分 有限數據類型
第10章 積類型 64
10.1 空積與二元積 64
10.2 有限積 65
10.3 原始互遞歸 66
10.4 注記 67
習題 67
第11章 和類型 69
11.1 空和與二元和 69
11.2 有限和 70
11.3 和類型的應用 71
11.3.1 void和unit 71
11.3.2 布爾類型 72
11.3.3 枚舉 72
11.3.4 選擇 73
11.4 注記 74
習題 74
第五部分 類型和命題
第12章 構造邏輯 78
12.1 構造語義 78
12.2 構造邏輯 79
12.2.1 可證性 79
12.2.2 證明項 81
12.3 證明的動態語義 82
12.4 命題即類型 83
12.5 注記 83
習題 83
第13章 經典邏輯 85
13.1 經典邏輯 85
13.1.1 可證性和可反駁性 86
13.1.2 證明和反駁 87
13.2 推導消去形式 89
13.3 證明的動態語義 90
13.4 排中律 91
13.5 雙重否定翻譯 92
13.6 注記 93
習題 94
第六部分 無限數據類型
第14章 泛型編程 96
14.1 引言 96
14.2 多項式類型算子 96
14.3 正類型算子 98
14.4 注記 99
習題 99
第15章 歸納類型與余歸納類型 101
15.1 示例 101
15.2 靜態語義 104
15.2.1 類型 104
15.2.2 表達式 105
15.3 動態語義 105
15.4 求解類型等式 106
15.5 注記 107
習題 107
第七部分 變量類型
第16章 多態類型的系統F 110
16.1 多態抽象 110
16.2 多態的可定義性 113
16.2.1 積與和 113
16.2.2 自然數 114
16.3 參數化概述 115
16.4 注記 116
習題 116
第17章 抽象類型 117
17.1 存在類型 117
17.1.1 靜態語義 118
17.1.2 動態語義 118
17.1.3 安全性 118
17.2 數據抽象 119
17.3 存在類型的可定義性 120
17.4 表示獨立性 120
17.5 注記 122
習題 122
第18章 高階種類 123
18.1 構造器和種類 123
18.2 構造器等同 125
18.3 表達式和類型 126
18.4 注記 126
習題 127
第八部分 部分性和遞歸類型
第19章 遞歸函數的系統PCF 130
19.1 靜態語義 131
19.2 動態語義 132
19.3 可定義性 133
19.4 有限數據結構和無限數據結構 135
19.5 完全性與部分性 135
19.6 注記 136
習題 136
第20章 遞歸類型的系統FPC 138
20.1 求解類型等式 138
20.2 歸納類型和余歸納類型 139
20.3 自指/自引用 141
20.4 狀態的起源 142
20.5 注記 143
習題 143
第九部分 動態類型
第21章 無類型的λ演算 146
21.1 λ演算 146
21.2 可定義性 147
21.3 Scott定理 149
21.4 無類型意味著單類型 150
21.5 注記 151
習題 151
第22章 動態定型 153
22.1 動態類型化PCF 153
22.2 變體和擴展 156
22.3 動態定型的批判 158
22.4
第2版前言
第1版前言
**部分 判斷和規則
第1章 抽象語法 2
1.1 抽象語法樹 2
1.2 抽象綁定樹 4
1.3 注記 8
習題 8
第2章 歸納定義 10
2.1 判斷 10
2.2 推理規則 10
2.3 推導 11
2.4 規則歸納 13
2.5 迭代歸納定義和聯立歸納定義 14
2.6 用規則定義函數 15
2.7 注記 15
習題 16
第3章 假言判斷與一般性判斷 17
3.1 假言判斷 17
3.1.1 可導性 17
3.1.2 可納性 18
3.2 假言歸納定義 20
3.3 一般性判斷 21
3.4 泛型歸納定義 22
3.5 注記 23
習題 23
第二部分 靜態語義和動態語義
第4章 靜態語義 28
4.1 語法 28
4.2 類型系統 29
4.3 結構性質 30
4.4 注記 31
習題 31
第5章 動態語義 33
5.1 轉換系統 33
5.2 結構化動態語義 34
5.3 上下文動態語義 36
5.4 等式動態語義 37
5.5 注記 39
習題 39
第6章 類型安全 40
6.1 保持性 40
6.2 進展性 41
6.3 運行時錯誤 42
6.4 注記 43
習題 43
第7章 求值動態語義 44
7.1 求值動態語義 44
7.2 結構化動態語義和求值動態語義
的關系 45
7.3 重溫類型安全 45
7.4 成本動態語義 46
7.5 注記 47
習題 47
第三部分 全函數
第8章 函數定義和值 50
8.1 一階函數 50
8.2 高階函數 51
8.3 求值動態語義和定義等同 53
8.4 動態作用域 54
8.5 注記 55
習題 55
第9章 高階遞歸的系統T 56
9.1 靜態語義 56
9.2 動態語義 57
9.3 可定義性 58
9.4 不可定義性 59
9.5 注記 61
習題 61
第四部分 有限數據類型
第10章 積類型 64
10.1 空積與二元積 64
10.2 有限積 65
10.3 原始互遞歸 66
10.4 注記 67
習題 67
第11章 和類型 69
11.1 空和與二元和 69
11.2 有限和 70
11.3 和類型的應用 71
11.3.1 void和unit 71
11.3.2 布爾類型 72
11.3.3 枚舉 72
11.3.4 選擇 73
11.4 注記 74
習題 74
第五部分 類型和命題
第12章 構造邏輯 78
12.1 構造語義 78
12.2 構造邏輯 79
12.2.1 可證性 79
12.2.2 證明項 81
12.3 證明的動態語義 82
12.4 命題即類型 83
12.5 注記 83
習題 83
第13章 經典邏輯 85
13.1 經典邏輯 85
13.1.1 可證性和可反駁性 86
13.1.2 證明和反駁 87
13.2 推導消去形式 89
13.3 證明的動態語義 90
13.4 排中律 91
13.5 雙重否定翻譯 92
13.6 注記 93
習題 94
第六部分 無限數據類型
第14章 泛型編程 96
14.1 引言 96
14.2 多項式類型算子 96
14.3 正類型算子 98
14.4 注記 99
習題 99
第15章 歸納類型與余歸納類型 101
15.1 示例 101
15.2 靜態語義 104
15.2.1 類型 104
15.2.2 表達式 105
15.3 動態語義 105
15.4 求解類型等式 106
15.5 注記 107
習題 107
第七部分 變量類型
第16章 多態類型的系統F 110
16.1 多態抽象 110
16.2 多態的可定義性 113
16.2.1 積與和 113
16.2.2 自然數 114
16.3 參數化概述 115
16.4 注記 116
習題 116
第17章 抽象類型 117
17.1 存在類型 117
17.1.1 靜態語義 118
17.1.2 動態語義 118
17.1.3 安全性 118
17.2 數據抽象 119
17.3 存在類型的可定義性 120
17.4 表示獨立性 120
17.5 注記 122
習題 122
第18章 高階種類 123
18.1 構造器和種類 123
18.2 構造器等同 125
18.3 表達式和類型 126
18.4 注記 126
習題 127
第八部分 部分性和遞歸類型
第19章 遞歸函數的系統PCF 130
19.1 靜態語義 131
19.2 動態語義 132
19.3 可定義性 133
19.4 有限數據結構和無限數據結構 135
19.5 完全性與部分性 135
19.6 注記 136
習題 136
第20章 遞歸類型的系統FPC 138
20.1 求解類型等式 138
20.2 歸納類型和余歸納類型 139
20.3 自指/自引用 141
20.4 狀態的起源 142
20.5 注記 143
習題 143
第九部分 動態類型
第21章 無類型的λ演算 146
21.1 λ演算 146
21.2 可定義性 147
21.3 Scott定理 149
21.4 無類型意味著單類型 150
21.5 注記 151
習題 151
第22章 動態定型 153
22.1 動態類型化PCF 153
22.2 變體和擴展 156
22.3 動態定型的批判 158
22.4
展開全部
實用編程語言理論基礎(原書第2版) 作者簡介
---作者簡介--- 羅伯特·哈珀(Robert Harper) 卡內基·梅隆大學計算機科學系教授，他的主要研究興趣是類型論在編程語言的設計與實現中的應用，以及其元理論的機械化。Harper是Allen Newell卓越研究獎章和Herbert A. Simon卓越教學獎的獲得者，并且是ACM會士。 ---譯者簡介--- 張昱 博士，中國科學技術大學計算機科學與技術學院、網絡空間安全學院副教授。研究興趣包括程序設計語言、操作系統和并行計算等，特別是面向人工智能和量子計算等新領域的編程系統、軟件分析、異構計算與系統優化等。 胡明哲 中國科學技術大學網絡空間安全學院博士研究生。主要研究方向為多語言軟件的程序分析。
書友推薦
- >
唐代進士錄
- >
名家帶你讀魯迅:朝花夕拾
- >
企鵝口袋書系列·偉大的思想20:論自然選擇(英漢雙語)
- >
巴金－再思錄
- >
中國人在烏蘇里邊疆區:歷史與人類學概述
- >
月亮與六便士
- >
伊索寓言-世界文學名著典藏-全譯本
- >
伯納黛特,你要去哪(2021新版)
本類暢銷
