Congratulations: We've made it to the end!

ふりかえり

ここまでとても多くのことを学んできました。 簡単に振り返ってみましょう。

• 関数プログラミング
  • 「宣言的」プログラミング（変更可能な配列やポインタなどによるループではなく、不変データ構造上の再帰）
  • 高階関数
  • 多相性

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

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

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

• Coq、産業用途に耐え得る証明支援器
  • 関数型のコア言語
  • 基礎となるタクティック
  • 自動化

これからの指針

もしここまでの内容に興味を抱いたなら、続きとして「ソフトウェアの基礎」のシリーズに二つの選択肢があります。

• 「プログラミング言語の基礎(Programming Language Foundations)」（この本とほとんど同じ著者たちに寄って書かれた第二巻）では、院生向けのプログラミング言語理論が説明されています。 例えばホーア論理や操作的意味論、型システムなどについてです。
• 「検証済み関数型アルゴリズム(Verified Functional Algorithms)」（Andrew Appelによる第三巻）では、Coqによる関数型プログラミングとプログラム検証について説明されています。 一般的なデータ構造に関して広く、検証という視点を交えて述べられています。

その他の資料

その他に先に進む資料としてよいものをいくつか...

• この本のオプションの章。 目次と依存関係のページを眺めてみてください。
• Coqに関する疑問には、Stack Overflowの #coq タグの情報が非常に有用です。 （訳注：日本語のStack Overflowもあるので、そちらも参照すると良いでしょう）
• 関数型プログラミングについてよい本をいくつか:
  • Learn You a Haskell for Great Good, by Miran Lipovaca Lipovaca 2011 (Bib.v内) （和訳：すごいHaskell たのしく学ぼう！）
  • Real World Haskell, by Bryan O'Sullivan, John Goerzen, and Don Stewart O'Sullivan 2008 (Bib.v内) （和訳：Real World Haskell ―― 実戦で学ぶ関数型言語プログラミング）
  • その他、Haskell、OCaml、Scheme、Racket、Scala、F sharpなどなどでの素晴らしい本
• Coqについての資料:
  • Certified Programming with Dependent Types, by Adam Chlipala Chlipala 2013 (Bib.v内)
  • Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Casteran Bertot 2004 (Bib.v内)
• 実際の重要なソフトウェアに対する検証の適用について、第二巻「プログラミング言語の基礎」のあとがきの章に挙げています。
• Coqを用いて検証済みシステムを構築するという話については、2017年のDeepSpec Summer Schoolの講義資料が有用でしょう。 https://deepspec.org/event/dsss17/index.html