Agda 証明支援系言語 slide: Agda 入門 Haskell っぽくて 依存型 がある 命題を表す論理式を型として定義できる 証明したい命題 == 関数の型 命題の証明 == 関数の定義 で表す. 関数と命題の対応を Curry-Howard Isomorphism Agda - mrsekut-p