ふりかえり...

関数プログラミング
- 「宣言的」プログラミング(永続データ構造上の再帰)
- 高階関数
- 多相性
Coq、産業用途に耐え得る証明支援器

論理学、ソフトウェア工学の数学的基盤:

                論理学                        微積分学
        --------------------   =   ----------------------------
            ソフトウェア工学                  機械/土木工学

帰納的に定義された集合と関係
帰納的証明
証明オブジェクト

プログラミング言語の基礎
- 以下を精密に定めるための記法と定義法
  - 抽象構文
  - 操作的意味
    - ビッグステップスタイル
    - スモールステップスタイル
  - 型システム
- ホーア論理
- プログラム同値性
- 型システムの基本的メタ理論
  - 進行と保存
  - 動的にアロケートされるヒープを持つ言語の型健全性
- サブタイプ理論

さらなる読み物

次のステップに適したものをいくつか...

Types and Programming Languages, by Benjamin C. Pierce. MIT Press, 2002.
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Castéran. Springer-Verlag, 2004.
Certified Programming with Dependent Types, by Adam Chlipala. A draft textbook on practical proof engineering with Coq, available from his web page.
Practical Foundations for Programming Languages, by Robert Harper. Manuscript, available from his web page.
The Formal Semantics of Programming Languages: An Introduction, by Glynn Winskel. MIT Press, 1993.
Foundations for Programming Languages, by John C. Mitchell. MIT Press, 1996.

Postscript_J: あとがき

ふりかえり...

さらなる読み物