Imogen is a theorem prover for intuitionistic logic. There are currently three versions:
The SML version is by far the most mature, and handles first-order intuitionistic logic, and has some naive support for linear and ordered logic. The Haskell version supports propositional intuitionistic logic and is significantly slower than the corresponding SML implementation. The Scala version is in its initial stages.