Motivation.

The aim of this implementation was first to implement Krivine's Af2 [1,2,3] type system, that is a system which allows to derive programs for proofs of their specifications.

The aim is now also to realize a Proof Checker used for teaching purposes in mathematical logic or even in ``usual'' mathematics.

The requirements for this new proof assistant are (it will be very difficult to reach all of them):

• Most of the ``usual'' mathematics should be feasible in this system. Actually is basically higher order classical logic, a more expressive (but not stronger) extension of the theory of simple types due to Ramsey [6]<sup>1.1</sup>. Feasability is probably much more a probleme of ``ergonomics'' than a probleme of logical strength.

  Anyway it is always possible to represent any first order theory, you can add axioms and first order axiom's schematas are replaced by second order axioms. You can represent this way set theory ZF in ^1.2.

• The manipulation of the system should be as intuitive as possible. Thus, we shall try to have a simple syntax and a comprehensive way to build proofs within our system. All of this should be accessible for any mathematician with a minimal learning.

• For programs extraction, we already know that provide enough functions (all functions provably total in higher order arithmetics) but we also need an efficient way to extract programs which should guaranty the fidelity to the specified algorithm and a good efficiency. The system will be credible only after bootstrapping which is the final (and long term) goal of this implementation !