Classical mathematics for a constructive world

DOI10.1017/S0960129511000132zbMath1263.03009arXiv1008.1213OpenAlexW2134649613MaRDI QIDQ3094179

Russell O'Connor

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1008.1213

zbMATH Keywords

classical function spacesinteractive theorem provingdependent type theoryclassical reasoningconstructive logic as an extension of classical logicconstructive reasoningweak value monad

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other constructive mathematics (03F65)

Cites Work

• A course in constructive algebra
• Strong functors and monoidal monads
• The Dedekind reals in abstract Stone duality
• A Modular Formalisation of Finite Group Theory
• Certified Exact Transcendental Real Number Computation in Coq
• Automated Machine-Checked Hybrid System Safety Proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Classical mathematics for a constructive world