Agda 入門
証明支援系の言語である Agda の入門を目的としています 具体的には Agda による証明の方法を知る 実際に自然数に対する演算の証明を追う ことをしていきます 証明支援系と呼ばれる分野の言語です 他には Coq などがあります Haskell で実装されています 型が非常に強力で表現力が高いです 命題や仕様を表す論理式を型として定義することができます 例えば 1 + 1 = 2 とか Agda における証明は 証明したい命題 == 関数の型 命題の証明 == 関数の定義 として定義します 関数と命題の対応を Curry-Howard Isomorphism と言います どうしてプログラムで証明できるかというと (命題 と 定義) は (仕様 と 実装) のように対応します int chars_to_int(char * chars) つまり char * から int は作れる、という
Agda 入門＠ProofSummit 2011
The document summarizes features and updates in the Agda proof assistant. It discusses Agda tactics, the module system, compilation to Haskell and Epic, sized types, irrelevant declarations, termination checking, instance arguments, pattern matching lambdas, and plans for upcoming releases including JavaScript compilation and pattern matching lambdas. It also demonstrates some Agda code examples.R
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
