A *(logic) theorem proof-assistant built atop _(Haskell), with support for _(tactic)s and subtyping. It is based on the logic of Pure Type Systems, which allows experimentation with various _(type system)s, for logics and _(programming languages), at run-time.

See the _(Yarrow home page| http://www.cs.kun.nl/~janz/yarrow/).