Famously, theThe type of call/cc (which may be realized with the 𝜆𝜇-calculus) corresponds with Peirce's Law, which implies LEM. Recently I learned through anThis answer by Pierre-Marie Pédrot thatexplains how Markov's principle (which follows from LEM) corresponds with a scheme which can be implemented with statically-bound exceptions.
LEM and call/cc come with severe difficulties from both a proof assistant andrealized by the programming language point of view, so it is often implemented as an axiom instead of a rule; Markov's principle and exceptions might come with fewer difficultiesDialectica interpretation or [statically-bound exceptions].
What other axioms have a computational interpretation? What difficulties might prevent them from being implemented by a proof assistant?
