『プログラミング言語の形式的意味論入門』
https://gyazo.com/ee80bbb525b5f3744f37aab56958d652
2023/1/30
まえがき
第1章 集合論の基礎
1.1 論理に関する記法／1.2 集合／1.3 関係と関数／1.4 参考文献
2.1 IMP――簡易命令型言語／2.2 算術式の評価／2.3 ブール式の評価／2.4 コマンドの実行／2.5 簡単な性質の証明／2.6 別の操作的意味論／2.7 参考文献
第3章 帰納法の原理
第4章 帰納的な定義
4.1 規則帰納法／4.2 特殊な規則帰納法／4.3 操作的意味論のための証明規則／4.4 演算とその最小不動点／4.5 参考文献 第5章 IMPの表示的意味論
第6章 IMPの公理的意味論
6.1 基本的なアイデア／6.2 表明言語Assn／6.3 表明の意味論／6.4 部分正当性のための証明規則／6.5 健全性／6.6 ホーア規則の使い方の例／6.7 参考文献 第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章 再帰の技法
第11章 高階型を持つ言語
11.1 先行評価のための言語／11.2 先行評価の操作的意味論／11.3 先行評価の表示的意味論／11.4 先行評価の意味論の一致／11.5 遅延評価のための言語／11.6 遅延評価の操作的意味論／11.7 遅延評価の表示的意味論／11.8 遅延評価の意味論の一致／11.9 不動点演算子／11.10 観測と完全抽象性／11.11 直和／11.12 参考文献 第12章 情報システム
12.1 再帰型／12.2 情報システム／12.3 閉集合族とScott前領域／12.4 情報システムのなすcpo／12.5 情報システムの構成／12.6 参考文献
付録A 不完全性と決定不能性
A.1 計算可能性／A.2 決定不能性／A.3 ゲーデルの不完全性定理／A.4 万能プログラム／A.5 Matijasevicの定理／A.6 参考文献
参考文献
監訳者あとがき
索引