Yarrow

Yarrow is an interactive proof assistant (proof editor) based on Pure Type Systems. The whole system is written in Haskell.