The `` Proof Checker'' is an implementation of higher order logic, inspired by Krivine's type system (see section 1.1), and designed by Christophe Raffalli. is a Proof assistant based on High Order logic and it is eXtensible.
One of the principle of this proof assistant is to be as user friendly as possible and so to need a minimal learning time. The current version is still experimental but starts to be really usable. It is a good idea to try it and make comments to improve the future releases.
Actually is mainly a proof editor for higher order logic. It is used this way to teach logic in the mathematic department from ``Université de Savoie''.
The implementation uses the Objective-Caml language. You will find in the chapter 10 the instruction to install .