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.