Galculator

The Galculator is a prototype of a proof assistant based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs.

It is written in the Haskell programming language resorting to many language extensions, specially GADTs (Generalized Algebraic Data Types).