Haskellで書かれたtheorem prover

http://www.haskell.org/haskellwiki/Libraries_and_tools/Theorem_provers
一杯ありすぎです

そんな中で、唯一スタンドアローンなアプリケーションではなく、ライブラリであるIvor(なんて読むんだ)が楽しそうな
http://www.dcs.st-and.ac.uk/~eb/ivor.php

ECC(多分extended calculus of construction)に似た型理論って言われてもわかんないよ。つか、CCシリーズって一杯あるけど、何が違うんだか