型システム入門 プログラミング言語と型の理論

前表紙
株式会社 オーム社, 2013/03/26 - 528 ページ

 

型システムを理解するうえでの定番書を翻訳型システムとは、プログラミング言語の安全性や効率を高めるうえで重要な理論・手法です。本書は、その型システムについて基礎的な話題を網羅し、実装例を交えて丁寧に解説したThe MIT Press発行の解説書“Types And Programming Languages”（TAPL）を翻訳したものです。言語設計者や学生だけでなく、静的型付言語を深く理解して活用したいプログラマーにとっても貴重な情報となっています。このような方におすすめ情報科の学生、研究者
静的型付言語を利用するプログラマー
日本語版に寄せて
監訳者序文
実用的情報
序文
謝辞
第1章 はじめに
第2章 数学的準備
■第1部 型無しの計算体系
第3章 型無し算術式
第4章 算術式のML実装
第5章 型無しラムダ計算
第6章 項の名無し表現
第7章 ラムダ計算のML実装
■第2部 単純型
第8章 型付き算術式
第9章 単純型付きラムダ計算
第10章 単純型のML実装
第11章 単純な拡張
第12章 正規化
第13章 参照
第14章 例外
■第3部 部分型付け
第15章 部分型付け
第16章 部分型付けのメタ理論
第17章 部分型付けのML実装
第18章 事例：命令的オブジェクト
第19章 事例：Featherweight Java
■第4部 再帰型
第20章 再帰型
第21章 再帰型のメタ理論
■第5部 多相性
第22章 型再構築
第23章 全称型
第24章 存在型
第25章 System F のML実装
第26章 有界量化
第27章 事例：命令的オブジェクト再考
第28章 有界量化のメタ理論
■第6部 高階の型システム
第29章 型演算子とカインド
第30章 高階多相
第31章 高階部分型付け
第32章 事例：純粋関数的オブジェクト
付録A 演習の解答
付録B 記法
参考文献
訳語集
規則図一覧
索引
 

ページのサンプル

目次

第1章はじめに
1
12 型システムで何ができるか
3
13 型システムと言語設計
7
14 歴史の概要
8
第2章数学的準備
11
22 順序集合
12
23 列
13
24 帰納法
14
195 性質
204
196 オブジェクト表現対組み込みのオブジェクト
205
197 注記
206
第IV部再帰型
207
第20章再帰型
209
201 例
210
202 形式的議論
215
203 部分型付け
218

第I部型無しの計算体系
15
第3章型無し算術式
17
32 構文
19
33 項に関する帰納法
21
34 意味論のスタイル
24
35 評価
25
36 注記
32
第4章算術式のML実装
35
42 評価
36
43 最後に
38
第5章型無しラムダ計算
39
52 ラムダ計算でのプログラミング
44
53 形式的議論
52
54 注記
55
第6章項の名無し表現
57
61 項と文脈
58
62 シフトと代入
59
63 評価
61
第7章ラムダ計算のML実装
63
72 シフトと代入
65
73 評価
66
第II部単純型
67
第8章型付き算術式
69
82 型付け関係
70
83 安全性進行+保存
72
第9章単純型付きラムダ計算
75
92 型付け関係
76
93 型付けの性質
78
94 CurryHoward対応
82
95 型消去と型付け可能性
83
96 Curryスタイル対Churchスタイル
84
第10章単純型のML実装
85
102 項と型
86
第11章単純な拡張
89
112 Unit型
90
逐次実行とワイルドカード
91
114 型指定
92
115 let束縛
94
116 二つ組
95
117 組
97
118 レコード
98
119 和
100
1110 バリアント
103
1111 一般的再帰
109
1112 リスト
111
第12章正規化
113
122 注記
116
第13章参照
117
132 型付け
121
134 ストア型付け
124
135 安全性
128
136 注記
130
第14章例外
133
142 例外の処理
135
第III部部分型付け
139
第15章部分型付け
141
152 部分型関係
142
153 部分型付けと型付けに関する性質
147
154 Top型とBottom型
149
155 部分型付けとその他の機能
151
156 部分型付けに対する型強制意味論
157
157 交差型と合併型
161
158 注記
162
第16章部分型付けのメタ理論
163
161 アルゴリズム的部分型付け
164
162 アルゴリズム的型付け
166
163 結びと交わり
170
164 アルゴリズム的型付けとBottom型
172
第17章部分型付けのML実装
173
173 型付け
174
命令的オブジェクト
177
182 オブジェクト
179
183 オブジェクト生成器
180
185 インスタンス変数のグループ化
181
187 インスタンス変数の付加
183
188 スーパークラスのメソッド呼び出し
184
1810 selfを介したオープンな再帰
185
1811 オープンな再帰と評価順序
186
1812 より効率的な実装
189
1813 要点のまとめ
191
1814 注記
192
Featherweight Java
193
192 概観
194
193 名前的型システムと構造的型システム
196
194 定義
198
第21章再帰型のメタ理論
221
212 有限型と無限型
223
213 部分型関係
224
214 推移律に関する余談
227
215 所属性検査
228
216 より効率的なアルゴリズム
232
217 正則木
235
218 μ型
236
219 部分式の数え上げ
240
指数オーダーアルゴリズム
243
2111 同型再帰型の部分型付け
245
2112 注記
246
第V部多相性
247
第22章型再構築
249
222 型変数についての二つの視点
250
223 制約に基づいた型付け
251
224 単一化
256
225 主要型
258
226 暗黙の型注釈
259
227 let多相
260
228 注記
264
第23章全称型
267
233 System F
268
234 事例
270
235 基本的な性質
277
236 型消去型付け可能性型再構築
278
237 型消去と評価順序
280
238 制限されたSystem F
281
239 パラメータ性
282
2311 注記
283
第24章存在型
285
242 存在型によるデータ抽象
288
243 全称型で存在型を表現する
295
244 注記
297
第25章 System FのML実装
299
253 項
301
254 評価
302
255 型付け
303
第26章有界量化
305
262 定義
306
263 例
310
264 安全性
314
265 有界存在型
318
266 注記
320
命令的オブジェクト再考
323
第28章有界量化のメタ理論
329
282 最小型付け
330
の部分型付け
332
の部分型付け
334
の決定不能性
337
286 結びと交わり
340
287 有界存在量化
343
288 有界量化とBottom型
344
第VI部高階の型システム
345
第29章型演算子とカインド
347
292 定義
352
第30章高階多相
355
302 例
357
303 性質
358
304 制限されたFω
364
依存型
365
第31章高階部分型付け
369
312 定義
370
313 性質
373
純粋関数的オブジェクト
375
322 部分型付け
376
323 有界量化
377
324 インターフェイス型
378
325 オブジェクトにメッセージを送る
379
326 単純クラス
380
327 多相更新
381
328 インスタンス変数の追加
383
329 selfを伴ったクラス
384
3210 注記
386
付録
387
付録A 演習の解答
389
付録B 記法
449
B3 名付けと添字の規約
450
参考文献
451
訳語集
485
規則図一覧
490
索引
492
著者監訳者訳者について
504
奥付
505
著作権

書誌情報

書籍名型システム入門 プログラミング言語と型の理論
著者Benjamin C. Pierce
翻訳住井 英二郎 , 遠藤 侑介 , 酒井 政裕 , 今井 敬吾 , 黒木 裕介 , 今井 宜洋 , 才川隆文 , 今井 健男
出版社株式会社 オーム社, 2013
ISBN4274069117, 9784274069116
ページ数528 ページ
  
引用のエクスポートBiBTeX EndNote RefMan