2011-01-01から1年間の記事一覧
この記事はTheorem Proving Advent Calendarの7日目の記事である。静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが…
VSTTE (Verified Software: Theories, Tools and Experiments) 2012 という学会の併設イベントでソフトウェア検証コンテストというものが開催されることを前日に id:keigoi さんに教えてもらって参加してみた。日時は日本時間で11月9日の0時から48時間。初め…
fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。 Definition xs := …
