2011-12-01から1ヶ月間の記事一覧

証明された証明支援器をScalaで書いてみた

この記事はTheorem Proving Advent Calendarの7日目の記事である。静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが…