The use of certain non-constructive logical constructs such as excluded middle and Peirce's law can be computationally interpreted as non-local control operators such as call-with-continuation (call/cc).
In [5] a heuristic search algorithm, conflict-directed back-jump, is developed in a Nuprl like type theory extended to extract call/cc from occurrences of Peirce's law. The computationally significant portions of the proof we formalized in an extended Nuprl system and the extracted term was translated into Scheme.
The goal of this part of the research is to build on [5] and establish methodology for the routine (but limited) use of non-constructive constructs in Nuprl proofs to yield efficient programs that utilize non-local control.