定理証明とか形式手法について調べてることをまとめる

ET2009で初めて知った形式手法が今マイブームなので、最近調べている事をまとめる。

 

-----Web上の記事-----

[Q&A]関数型プログラミング言語、よくある疑問

"関数型プログラミング言語は、ソフトウエアの仕様を厳密に記述する手法「形式手法」と相性が良いと言われている。形式手法の一種に「定理証明」があり、これはあるシステムが仕様通りになっていることを、個別のテストケースで確かめるのではなく、どんな時でも仕様通りとなることを論理的に証明するアプローチである。「Coq」という定理証明の支援ツールがあり、そこで定理証明を行った後、仕様通りであることが確かめられたコードをHaskellなどの形式で生成するといった取り組みを、一部の先進的な企業が行っている。"

これが形式手法マイブーム再燃の原因

 

Coqで学習するならどのページがいい?って聞かれたときのメモ

かなり充実しているので優先度高し

 

プログラミング Coq 〜絶対にバグのないプログラムの書き方〜

充実していて実用的なCoq入門

 

Haskell/カリー=ハワード同型対応

WikipediaのC-H同型対応の記事はほぼリファレンスで僕みたいな初心者には残念

 

Curry-Howard Isomorphism -Derive Your Dreams-

より分かりやすいC-H同型対応

 

Coquet: a Coq library for verifying hardware

ハードウェアを証明しようっていう論文。

組み込みとかそっち系のほうが証明や形式手法が先行しているイメージ。

 

edubase stream

しばらく前に登録してたけど全然見ていなかった。

でも形式手法とかが充実しているので見てみる。

 

Coq/tactics

非公式の一覧(日本語)

 

Coq庵

というイベント

 

[Why3] Install of  Why3 Tools (Theorim Prover Advent Calendar)

このアドベントカレンダーも見返しておくべきか

 

-----Slidshare-----

 
名古屋こわい。
あとOCamlは必修らしいな。