Document Actions
Galculator
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.
The prototype of Galculator is being developed under an ongoing PhD project. It is written in the Haskell programming language resorting to many language extensions, specially GADTs (Generalized Algebraic Data Types).
Download
The sources can be downloaded from the SVN repository. The current implementation is unstable and experimental. We plan to release a fully operational prototype as soon as possible.Note: Building Galculator requires GHC Haskell compiler, version 6.8.x.
Documentation
The documentation of the tool is still missing. We hope to solve that soon.
New developments
Currently, we are working in the automatic derivation of the so-called “free- theorems” of polymorphic functions and their application to proofs. Moreover, more complex constructions of Galois connections are also being studied. Fi- nally, we plan to integrate the Galculator with a theorem prover, namely Coq.
Contact
For any information, please contact Paulo Silva
email
homepage