Sciweavers

LICS
2010
IEEE

An Intuitionistic Logic that Proves Markov's Principle

13 years 2 months ago
An Intuitionistic Logic that Proves Markov's Principle
—We design an intuitionistic predicate logic that supports a limited amount of classical reasoning, just enough to prove a variant of Markov’s principle suited for predicate logic. At the computational level, the extraction of an existential witness out of a proof of its double negation is done by using a form of statically-bound exception mechanism, what can be seen as a direct-style variant of Friedman’s A-translation. Keywords-Markov’s principle; intuitionistic logic; proof-asprogram correspondence; exceptions
Hugo Herbelin
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LICS
Authors Hugo Herbelin
Comments (0)