強く型付けされた関数型プログラミング言語におけるモデル検査の妥当性？

Question

私は現在モデル検査（モーダルロジック、LTL、CTL、SALモデルチェッカーなど）を学んでいます。私は余暇のうちに依存型をサポートする強く型付けされた関数型プログラミング言語であるIdrisについて学んでいます。私はモデル検査とIdrisの両方を検討しているので、Idrisが正式な方法とモデル検査にどのように関係しているか興味があります。

モデル検査について学ぶとき、ほとんどの例は、命令的に書かれたシステムやハードウェアコンポーネントの検証に関するものです。だから私は強く型付けされた関数型プログラミング言語、特にIdrisのような依存型言語でのモデル検査の妥当性に疑問を覚えていますが、型チェッカーはすでに正当性を検証する上で素晴らしい仕事をしているようです。 しかし私の直感は、モデルチェックがおそらく終了の約束を与えない部分的な機能に関係するかもしれないと私に伝えます。

Idrisのような強く従属型のプログラミング言語を使用する場合、モデル検査は適切ですか？

Answer 1

モデルチェックは、ハードウェアの検証と命令型（多くの場合並行）のプログラムでよく使用されます。このプログラムの起点もこの領域にあります。機能的なプログラムでは、精巧な型システム技術が検証のために広く使用されている。しかし、彼らはしばしば多くのアノテーションを必要とするか、または「誤ったポジティブ」を生成し、結果として「正しい」プログラムを反論することがあります。モデル検査はこれらの注釈を必要とせず、より具体的な質問に答えることもできます。 私はこの分野の専門家ではありませんが、タイプシステムとモデル検査のテクニックは、機能プログラムのために組み合わされているようです。 あなたは現在の研究に興味があり、関数型プログラムのモデル検査のために近づくと、材料オンラインのたくさんの素晴らしいコースがあります：

http://www.cs.ox.ac.uk/people/luke.ong/personal/EWSCS13

コースはルークオング、大手の一つで作成されていますフィールドの研究者。