Proof assistant written in Haskell, utilizing Calculus of Constructions (CoC), similar to (a simpler version of) that used in the famous Coq. Capon has a REPL, soon a batch mode and a dream of a language server.
Capon does not intend to compete with any serious proof assistant, it is merely my playground for getting to know Haskell better and to learn some type theory in practice. It began as a final project on FP course, I only develop it further because it is so much fun.
git clone https://github.com/Telpenarmo/capon.git
cd capon
cabal build # to just build
cabal run capon # to run
To be added later.
"Complete Bidirectional Typing for the Calculus of Inductive Constructions"