Postscript_J: あとがき¶
ふりかえり...¶
関数プログラミング - 「宣言的」プログラミング(永続データ構造上の再帰)
高階関数
多相性
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 andPierre 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.