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.