Imp: Simple Imperative Programs

• Arithmetic and Boolean Expressions
  • Syntax
  • Evaluation
  • Optimization
• Coq Automation
  • Tacticals
  • Defining New Tactic Notations
  • The omega Tactic
  • A Few More Handy Tactics
• Evaluation as a Relation
  • Inference Rule Notation
  • Equivalence of the Definitions
  • Computational vs. Relational Definitions
• Expressions With Variables
  • States
  • Syntax
  • Notations
  • Evaluation
• Commands
  • Syntax
  • Desugaring notations
  • The Locate command
  • More Examples
• Evaluating Commands
  • Evaluation as a Function (Failed Attempt)
  • Evaluation as a Relation
  • Determinism of Evaluation
• Reasoning About Imp Programs
• Additional Exercises

Maps: Total and Partial Maps

• The Coq Standard Library
• Identifiers
• Total Maps
• Partial maps

Preface: 前書き

• ようこそ
• 概要
  • プログラム検証
  • 型システム
  • 参考文献
• 教育関係者へ
• Thanks

Equiv: プログラムの同値性

• 振る舞い同値性
  • 定義
  • 簡単な例
• 振る舞い同値の性質
  • 振る舞い同値は同値関係である
  • 振る舞い同値は合同関係である
• プログラム変換
  • 定数畳み込み変換
  • 定数畳み込みの健全性
• 非等価性の証明
• Extended Exercise: Nondeterministic Imp
• さらなる練習問題

Hoare: ホーア論理、第一部

• 表明
• ホーアの三つ組
• 証明規則
  • 代入
  • 帰結
  • 余談: eapply タクティック
  • Skip
  • コマンド合成
  • 条件分岐
  • ループ
• Summary
• Additional Exercises

Hoare2: Hoare Logic, Part II

• Decorated Programs
  • Example: Swapping Using Addition and Subtraction
  • Example: Simple Conditionals
  • Example: Reduce to Zero
  • Example: Division
• Finding Loop Invariants
  • Example: Slow Subtraction
  • Exercise: Slow Assignment
  • Exercise: Slow Addition
  • Example: Parity
  • Example: Finding Square Roots
  • Example: Squaring
  • Exercise: Factorial
  • Exercise: Min
  • Exercise: Power Series
• Weakest Preconditions (Optional)
• Formal Decorated Programs (Advanced)
  • Syntax
  • Extracting Verification Conditions
  • Automation
  • Examples
  • Further Exercises

HoareAsLogic: 論理としてのホーア論理

• 定義
• 性質

Smallstep: スモールステップ操作的意味論

• おもちゃの言語
• Relations
  • 値
  • 強進行と正規形
• マルチステップ簡約
  • Examples
  • 正規形再び
  • ビッグステップとスモールステップの同値性
  • さらなる練習問題
• スモールステップ Imp
• 並行 Imp
• A Small-Step Stack Machine
• 余談: normalize タクティック

Types: 型システム

• 型付きの算術式
  • 構文
  • 操作的意味論
  • 正規形と値
  • 型付け
  • 進行
  • 型保存
  • 型の健全性
  • 追加演習

Stlc: 単純型付きラムダ計算

• • 概観
• 構文
  • 型
  • 項
• 操作的意味論
  • 値
  • 置換
  • 簡約
  • 例
• 型付け
  • コンテキスト
  • 型付け関係
  • 例

StlcProp: Properties of STLC

• Canonical Forms
• Progress
• Preservation
  • Free Occurrences
  • Substitution
  • Main Theorem
• Type Soundness
• Uniqueness of Types
• Additional Exercises
  • Exercise: STLC with Arithmetic

MoreStlc: 単純型付きラムダ計算についてさらに

• STLCの単純な拡張
  • 数値
  • let束縛
  • 対
  • Unit型
  • 直和
  • リスト
  • 一般再帰
  • レコード
• 練習問題: 拡張を形式化する
  • 例
  • 型付けの性質

Sub: サブタイプ

• 概念
  • 動機付け
  • サブタイプとオブジェクト指向言語
  • 包摂規則
  • サブタイプ関係
  • Exercises
• 形式的定義
• 中核部の定義
  • サブタイプ
  • 型付け
• 性質
  • サブタイプの反転補題(Inversion Lemma)
  • 正準形(Canonical Forms)
  • 進行
  • 型付けの反転補題
  • コンテキスト不変性
  • 置換
  • 保存
  • Records, via Products and Top
  • 練習問題
• 練習問題: 直積の追加

Typechecking: STLCの型チェッカ

• 型を比較する
• 型チェッカ
• Digression: Improving the Notation
• 性質
• Exercises

Records: STLCにレコードを追加する

• レコードを追加する
• レコードを形式化する
  • 例
  • 型付けの性質

References: 変更可能な参照の型付け

• 定義
• 構文
• プラグマティクス（語用論）
  • 副作用と順次処理
  • 参照と別名付け
  • 共有状態
  • オブジェクト
  • 参照と合成型
  • null参照
  • ガベージコレクション
• 操作的意味
  • 場所(Locations)
  • 記憶(Stores)
  • 簡約
• 型付け
  • 記憶の型付け
  • 型付け関係
• 性質
  • 型付けできる記憶
  • 記憶型付けを拡張する
  • 保存、最終的に
  • 置換補題
  • 代入は記憶型付けを保存する
  • 記憶についての弱化
  • 保存!
  • 進行
• 参照と非停止性
• さらなる練習問題

RecordSub: レコードのサブタイプ

• 中核部の定義
• サブタイプ
  • 定義
  • 例
  • サブタイプの性質
• 型付け
  • 型付けの例
  • 型付けの性質

Norm: STLCの正規化

• 言語
• 正規化
  • R_T の要素であるか否かは簡約によって変化しない
  • 型Tの項の閉じたインスタンスがR_Tに含まれる

LibTactics: 使いやすい汎用タクティックのコレクション

• Ltacによるプログラミングのための道具類
  • 等価継続
  • タクティックの型付けされない引数
  • タクティックのオプショナルな引数
  • タクティックのワイルドカード引数
  • ポジションマーカ
  • タクティックの引数のリスト
  • 補題のデータベース
  • その場での仮定の除去
  • 引数としての数値
  • タクティックをテストする
  • Testing evars and non-evars
  • ゴールにやり残しがないことのチェック
  • Evarを導入する補助関数
  • 仮定のタグ付け
  • 仮定のタグ付けをさらに
  • 項を解体する
  • 出現場所でのアクションと出現場所以外でのアクション
  • eqの別名
• intuitionのようにゴールを簡約するタクティック
• 後方/前方連鎖
  • 適用(Application)
  • 表明(Assertions)
  • 具体化と前方連鎖
  • 適用(application)の実験的タクティック
  • 仮定を追加する
  • トートロジーの適用
  • 等式を法とした適用
  • Absurd Goals
• 導入と一般化
  • 導入(Introduction)
  • Introduction using => and =>>
  • 一般化(Generalization)
  • 名前付け(Naming)
• 書き換え(Rewriting)
  • 置き換え(Replace)
  • Change
  • 名前変え(リネーム、Renaming)
  • 定義の展開(Unfolding)
  • 単純化(Simplification)
  • 簡約(Reduction)
  • 置換(Substitution)
  • proof irrelevance を扱うタクティック
  • 等式を証明する
• 反転(Inversion)
  • 基本反転(Basic Inversion)
  • 置換(substitution)を伴う反転(inversion)
  • 置換を伴う注入(Injection)
  • 置換を伴う反転と注入 -- おおざっぱな実装
  • 場合分け
• 帰納法(Induction)
• Coinduction
• 決定可能な等式
• 同値(Equivalence)
• N個の連言と選言
• タイプクラスのインスタンスを証明するためのタクティック
• 自動化起動のタクティック
  • Definitions for Parsing Compatibility
  • hint to Add Hints Local to a Lemma
  • jauto, 新しい自動化タクティック
  • 自動化タクティックの定義
  • 軽い自動化の構文解析
  • 強力な自動化の構文解析
• 証明コンテキストを整理するためのタクティック
  • 仮定の隠蔽
  • 仮定のソーティング
  • 仮定のクリア
• 開発目的のタクティック
  • サブゴールのスキップ
• 標準ライブラリとのコンパチビリティ

UseTactics: Coq用タクティックライブラリの簡単な紹介

• 命名とInversionの取り扱いについてのタクティック
  • タクティックintrov
  • タクティックinverts
• n-引数論理演算のためのタクティック
  • タクティック splits
  • タクティック branch
• 等式を扱うタクティック
  • タクティック asserts_rewrite と cuts_rewrite
  • タクティック substs
  • タクティック fequals
  • タクティック applys_eq
• 便利な略記法をいくつか
  • タクティック unfolds
  • タクティックfalseとtryfalse
  • タクティック gen
  • タクティックadmits、admit_rewrite、admit_goal
  • タクティック sort
• 高度な補題具体化のためのタクティック
  • letsのはたらき
  • applys、forwards、specializesのはたらき
  • 具体化の例
• まとめ

UseAuto: Coqの証明自動化の理論と実践

• 証明探索の基本性質
  • 証明探索の強さ
  • 基本
  • 連言
  • 選言
  • 存在限量
  • 否定
  • 等式
• 証明探索はどのようにはたらくか
  • 探索の深さ
  • バックトラック
  • ヒントを追加する
  • タクティックへの自動証明の統合
• 自動化による証明例
  • 決定性
  • STLC の保存
  • STLC の前進
  • ビッグステップとスモールステップ
  • STLCRef の保存
  • STLCRef の前進
  • サブタイプ
• 証明探索の進んだ話題
  • 補題を正しい方法で記述する
  • 証明検索中で定義を展開する
  • 不合理なゴールの証明の自動化
  • 推移性補題についての自動化
• 決定手続き
  • Omega
  • Ring
  • Congruence
• まとめ

PE: 部分評価

• 定数畳み込みを一般化する
  • 部分状態
  • 算術式
  • ブール式
• ループ以外のコマンドの部分評価
  • 代入
  • 条件分岐
  • 部分評価関係
  • 例
  • 部分評価の正しさ
• ループの部分評価
  • 例
  • 正当性
• フローチャートプログラムの部分評価
  • 基本ブロック
  • フローチャートプログラム
  • 基本ブロックとフローチャートプログラムの部分評価

Postscript: あとがき

• ふりかえり
• Looking Around
• これからの指針

Bib: Bibliography

• Resources cited in this volume