The MINLOG System
Documentation
The latest version
of MINLOG is MINLOG 4.0 and
the Documentation refers to this version. The articles instead make use of
Version 3.i. MINLOG 4.0 is an extension of this version featuring a slightly
different syntax.
Tutorial
A first introduction to the system is provided by the
Tutorial:
tutor.pdf
.
Reference Manual
For a more thorough description of MINLOG one should
consult the Reference Manual:
ref.pdf
Theory
Some information on the underlying theory of Minlog can be found
in Minimal Logic for Computable Functionals:
mlcf.pdf
Case Studies and Publications
- The greatest common divisor: a case study for program
extraction from classical proofs, U. Berger and H. Schwichtenberg
(Turin '95)
- Formal correctness proofs of functional programs: Dijkstra's
algorithm, a case study, H. Benl, H.Schwichtenberg (Marktoberdorf
'97)
- Proof theory at work: Program development in the Minlog
system, H. Benl, U. Berger, H. Schwichtenberg, M. Seisenberger, and
W. Zuber (Automated Deduction, W. Bibel and P.H. Schmitt, eds., Vol. II,
Kluwer 1998)
-
The Warshall Algorithm and Dickson's Lemma: Two Examples of
Realistic Program Extraction
,
U. Berger, H. Schwichtenberg, and M. Seisenberger, Journal of
Automated Reasoning 26, 2001, pp. 205–221
-
Program extraction from normalization proofs
,
U. Berger, S. Berghofer, P. Letouzey, and H. Schwichtenberg
(Final version in Studia Logica 82, 2006, pp. 27–51)
-
Minlog, H. Schwichtenberg (The Seventeen Provers of the World,
F. Wiedijk, ed., Springer Verlag, 2006, pp. 151–157)
-
Minlog - A Tool for Program Extraction Supporting
Algebras and Coalgebras
,
U. Berger, K. Miyamoto, M. Seisenberger, and H. Schwichtenberg
(CALCO 2011 Volume LNCS 6859, pp. 393–399)
