Yarrow
A logic theorem proof-assistant built atop Haskell, with support for tactics and subtyping. It is based on the logic of Pure Type Systems, which allows experimentation with various type systems, for logics and programming languages, at run-time.See the Yarrow home page.