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.