0 Contents

Contents
  Acknowledgements
1.  Introduction
   1.1.  Simultaneous free algebras
   1.2.  Partial continuous functionals
   1.3.  Primitive recursion, computable functionals
   1.4.  Decidable predicates, axioms for predicates
   1.5.  Minimal logic, proof transformation
   1.6.  Comparison with Coq and Isabelle
2.  Types, with simultaneous free algebras as base types
   2.1.  Generalitites for substitutions, type substitutions
   2.2.  Simultaneous free algebras as base types
3.  Variables
4.  Constants
   4.1.  Rewrite and computation rules for program constants
   4.2.  Recursion over simultaneous free algebras
   4.3.  Internal representation of constants
5.  Predicate variables and constants
   5.1.  Predicate variables
   5.2.  Predicate constants
   5.3.  Inductively deﬁned predicate constants
6.  Terms and objects
   6.1.  Normalization
   6.2.  Substitution
7.  Formulas and comprehension terms
8.  Assumption variables and constants
   8.1.  Assumption variables
   8.2.  Axiom constants
   8.3.  Theorems
   8.4.  Global assumptions
9.  Proofs
   9.1.  Constructors and accessors
   9.2.  Normalization
   9.3.  Substitution
   9.4.  Display
   9.5.  Classical logic
10.  Interactive theorem proving with partial proofs
   10.1.  Partial proofs
   10.2.  Interactive theorem proving
11.  Search
12.  Computational content of classical proofs
13.  Extracted terms
14.  Reading formulas in external form
   14.1.  Lexical analysis
   14.2.  Parsing
References
Index

Acknowledgements. The Minlog system has been under development since around 1990. My sincere thanks go to the many contributors: Holger Benl (Dijkstra algorithm, inductive data types), Ulrich Berger (very many contributions), Michael Bopp (program development by proof transformation), Wilfried Buchholz (translation of classical proof into intuitionistic ones), Laura Crosilla (tutorial), Matthias Eberl (normalization by evaluation), Dan Hernest (functional interpretation), Felix Joachimski (many contributions, in particular translation of classical proofs into intuitionistic ones, producing Tex output, documentation), Ralph Matthes (documentation), Karl-Heinz Niggl (program development by proof transformation), Jaco van de Pol (experiments concerning monotone functionals), Martin Ruckert (many contributions, in particular the MPC tool), Robert Stärk (alpha equivalence), Monika Seisenberger (many contributions, including inductive deﬁnitions and translation of classical proofs into intuitionistic ones), Klaus Weich (proof search, the Fibonacci numbers example), Wolfgang Zuber (documentation).