http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVs... You might also want to compare

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVs... You might also want to compare to Idris (and maybe Epigram, but its no longer in development). http://www.quora.com/How-does-Idris-compare-to-other-dependently-typed-programming-languages http://www.quora.com/How-does-Idris-compare-to-other-depende... http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram_or_idris_which_one_to_learn/ http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram... http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/ http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_... http://stackoverflow.com/questions/9472488/differences-between-agda-and-idris http://stackoverflow.com/questions/9472488/differences-betwe... All have pros and cons; i like that Idris can compile to JS (https://raichoo.github.io/posts/2014-01-28-improved.html https://raichoo.github.io/posts/2014-01-28-improved.html)