The MINLOG System
About the MINLOG System
MINLOG is based on first order natural deduction calculus. It is intended to reason about computable functionals, using minimal rather than classical or intuitionistic logic. The main motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are in fact treated as first class objects which can be normalized. If a formula is existential then its proof can be used for reading off an instance of it, or changed appropriately for program development by proof transformation. To this end MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined A-translation. The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.
How to get MINLOG
The latest beta version of MINLOG is available as a tar.gz file, from Subversion (for members of the working group) and as Debian packages.
MINLOG is implemented in SCHEME and runs under every SCHEME version supporting the Revised5 Report on the Algorithmic Language Scheme. MINLOG's favorite dialect is Petite Chez Scheme from Cadence Research Systems, which is freely distributed at the address http://www.scheme.com.
For further help to install MINLOG on your system, take a look at the installation instructions.
If you have any problems with the MINLOG system or suggestions please feel free to send an email to firstname.lastname@example.org.