Computer Science – Logic in Computer Science
Scientific paper
2010-08-03
Mathematical Structures in Computer Science (2011), 21: 861-882
Computer Science
Logic in Computer Science
v2: Final copy for publication
Scientific paper
10.1017/S0960129511000132
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 see several examples of how classical results can be applied to constructive mathematics. Finally, we will see how to extend this perspective from logic to mathematics by representing classical function spaces using a weak value monad.
No associations
LandOfFree
Classical Mathematics for a Constructive World does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Classical Mathematics for a Constructive World, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Classical Mathematics for a Constructive World will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-615529