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 lambda-calculus that can be used for this purpose. The systems are natural deduction systems, and use the propositions-as-types 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.