【飲食OK】Agda入門

ツイート

講師：河野 真治
担当：琉球大学工学部情報工学科並列信頼研
レベル：入門編
対象者：特になし
前提知識：特になし

比較的マイナーな定理証明支援系であるAgdaを紹介します。
AgdaはHaskellで書いてあり、Emacs をUser Interfaceとして用いる会話的な定理証明支援系です。
これを用いた簡単な定理の証明の実演を行います。

【カテゴリ】計算理論/証明/Emacs/Haskell