







Type Theories from Barendregt's Cube for Theorem
Provers
Anybody using a theorem prover or proof assistant will want to have
confidence that the system involved will not permit the derivation of false
results. On some occasions, there is more than usual need for this
confidence. This talk will discuss some logical systems based on typed
lambdacalculus that can be used for this purpose. The systems are natural
deduction systems, and use the propositionsastypes paradigm. Not only
are the underlying systems provably consistent, but additional unproved
assumptions from which a lot of ordinary mathematics can be derived can
also be proved consistent. Finally, the systems have few primitive
postulates that need to be programmed separately, so that it is easier for
a programmer to see whether the code really does program the systems
involved without errors.






