リストのconsの型をA -> list A -> list AではなくA -> list (list A) -> list Aにした型をHaskellとCoq/SSReflectで定義したいHaskellCoqssreflectリスト形式検証 はじめに 本記事はTPP2024で発表した内容になります。 リストlistの型は通常nilとconsの2つのコンストラクタから定義されますが、 型変数Aに対し、cons A型をA -> list A -> list AではなくA -> list (list A) -> list Aに変更した型をHaskellやCoq/SSreflectで定義する方法について記述します。 ソースはこちら Haskellで定義する まず、この型の名前をSSeqとしてHaskellで実装したものは以下のようになります。
目的 定理証明支援とは何かと現状の整理。 定理証明支援とは 定理証明支援とは数学の定理を自動で証明することではなく、ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである。 支援だから意味ないということでなく、最近の数学の証明は長くなり証明の検証が難しいのを助ける意味がある。定理証明支援の意義についてはこちらが詳しい。 また、信頼性が求めらる難しいアルゴリズムの検証、たとえばTLS(暗号通信)やRaft(分散合意アルゴリズム)のサーバーに利用されつつある。 ここでいう定理は大げさなものだけでなく、$1+1=2$、$0何か=0$、$ab=b*a$といった簡単なものを証明しながらどんどん積み上げていく。通常のプログラムと違うのは証明であるので使用する変数が整数ならそのすべての値について成り立つ定理を証明する。 定理を証明するのに使うツールは下記である。(他
Idris: A Language for Type-Driven Development Idris is a programming language designed to encourage Type-Driven Development. In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
