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.