a1 Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada and Microsoft Research – INRIA Joint Centre Email: [email protected]
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory, and classical reasoning is typically supported by adding additional non-constructive axioms. However, there is another perspective that views constructive logic as an extension of classical logic. This paper will illustrate how classical reasoning can be supported in a practical manner inside dependent type theory without additional axioms. We will show several examples of how classical results can be applied to constructive mathematics. Finally, we will show how to extend this perspective from logic to mathematics by representing classical function spaces using a weak value monad.
(Received July 11 2010)
(Revised December 15 2010)
(Online publication July 01 2011)