プログラミング言語の形式的意味論入門

本書は、Ｗｉｎｓｋｅｌによるプログラミング言語意味論の世界的標準教科書の邦訳である。前提知識をできるだけ少なくしつつ、プログラムの意味を数学的に定義・議論するための手法が解説されている。本書により、プログラミング言語理論関係の専門的な文献を読むための基礎を学ぶことができる。本書で身につけた基礎知識は、プログラミング言語研究の成果を理解し応用するために役立つはずである。

プログラミング言語の（形式的）意味論とは、プログラムの動作を数学によって厳密に定義し、その性質について議論するための枠組みのことである。プログラムを数学の俎上に載せることにより、プログラムやプログラミング言語を厳密に理解し、解析し、これらについて推論することができるようになる。この分野は近年実用化に向けて進んでいる形式手法の礎となり、またそれ自体、様々な数学概念が飛び交う興味深い一分野を形成してきた。

本書は、Winskelによるプログラミング言語意味論の世界的標準教科書の邦訳である。前提知識をできるだけ少なくしつつ、プログラムの意味を数学的に定義・議論するための手法が解説されている。本書により、プログラミング言語理論関係の専門的な文献を読むための基礎を学ぶことができる。本書で身につけた基礎知識は、プログラミング言語研究の成果を理解し応用するために役立つはずである。

目次

まえがき
第1章 集合論の基礎
1.1 論理に関する記法／1.2 集合／1.3 関係と関数／1.4 参考文献
第2章 入門：操作的意味論
2.1 IMP――簡易命令型言語／2.2 算術式の評価／2.3 ブール式の評価／2.4 コマンドの実行／2.5 簡単な性質の証明／2.6 別の操作的意味論／2.7 参考文献
第3章 帰納法の原理
3.1 数学的帰納法／3.2 構造帰納法／3.3 整礎帰納法／3.4 導出に関する帰納法／3.5 帰納的定義／3.6 参考文献
第4章 帰納的な定義
4.1 規則帰納法／4.2 特殊な規則帰納法／4.3 操作的意味論のための証明規則／4.4 演算とその最小不動点／4.5 参考文献
第5章 IMPの表示的意味論
5.1 動機／5.2 表示的意味論／5.3 二つの意味論の等価性／5.4 cpoと連続関数／5.5 Knaster-Tarskiの定理／5.6 参考文献
第6章 IMPの公理的意味論
6.1 基本的なアイデア／6.2 表明言語Assn／6.3 表明の意味論／6.4 部分正当性のための証明規則／6.5 健全性／6.6 ホーア規則の使い方の例／6.7 参考文献
第7章 ホーア規則の完全性
7.1 ゲーデルの不完全性定理／7.2 最弱事前条件と表現可能性／7.3 ゲーデルの不完全性定理の証明／7.4 検証条件／7.5 述語変換子／7.6 参考文献
第8章 領域理論入門
8.1 基本的な定義／8.2 例：ストリーム／8.3 cpoの構成手法／8.4 連続関数を定義するためのメタ言語／8.5 参考文献
第9章 再帰方程式
9.1 言語REC／9.2 値呼びの操作的意味論／9.3 値呼びの表示的意味論／9.4 値呼びの二つの意味論の等価性／9.5 名前呼びの操作的意味論／9.6 名前呼びの表示的意味論／9.7 名前呼びの二つの意味論の等価性／9.8 局所的な関数定義／9.9 参考文献
第10章 再帰の技法
10.1 Beki?の定理／10.2 不動点帰納法／10.3 整礎帰納法／10.4 整礎再帰／10.5 演習を一つ／10.6 参考文献
第11章 高階型を持つ言語
11.1 先行評価のための言語／11.2 　ほか

本の帯に関して

帯つきでの出荷はお約束しておりません。
商品ページに、帯のみに付与される特典物等の表記がある場合でも、確実に帯つきでの出荷はお約束しておりません。
また、帯は商品の一部ではなく「広告扱い」のため、帯の有無・破損による交換や返品は承っておりません。

版・表紙について

版・表紙（カバー）のご指定は承っておりません。ご注文いただくタイミングによっては、お届けする商品の版や表紙が商品ページ上のものとは異なる場合がございます。
また、初版にのみにお付けしている特典（初回特典、初回仕様特典）がある商品は、商品ページに特典の表記がされている場合でも、無くなり次第終了となります。