CoqとAgda

プログラミング言語

CoqはOCamlで書かれているようだ。

To compile Coq, you need:
* Objective Caml (3.07 ? version but 3.08.0).

http://coq.inria.fr/distrib1-eng.html

AgdaはHaskellで書かれているようだ。

Agda: Instruction(Mac)
Q: Agda doesn't work suddenly.
A: Did you uninstall Glasgow Haskell Compiler (GHC)?

http://unit.aist.go.jp/cvs/Agda/how-to-install-macosx.html

これをみるとMathematical度は同じくらい？
automation度はCoqの方が上？

Freek Wiedijk. Comparing mathematical provers
各種のシステムの大雑把な比較

http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20050929#p01