Search Algorithms in Type Theory
by James L. Caldwell, Ian Gent, and
Theoretical Computer Science, vol. 232, nos. 1-2, pp. 55-90, 2000.
In this paper, we take an abstract view of search by describing search procedures via particular kinds of proofs in type theory.