Search algorithms in type theory

In this paper, we take an abstract view of search by describing search proc edures via particular kinds of proofs in type theory. We rely on the proofs -as-programs interpretation to extract programs from our proofs. Using thes e techniques we explore, in depth, a large family of search problems by par ameterizing the specification of the problem. A constructive proof is prese nted which has as its computational content a correct search procedure for these problems. We show how a classical extension to an otherwise construct ive system can be used to describe a typical use of the nonlocal control op erator call/cc. Using the classical typing of nonlocal control we extend ou r purely constructive proof to incorporate a sophisticated backtracking tec hnique known as 'conflict-directed backjumping' (CBJ). A variant of this pr oof is formalized in Nupr1 yielding a correct-by-construction implementatio n of CBJ. The extracted program has been translated into Scheme and serves as the basis for an implementation of a new solution to the Hamiltonian cir cuit problem. This paper demonstrates a nontrivial application of the proof s-as-programs paradigm by applying the technique to the derivation of a sop histicated search algorithm; also, it shows the generality of the resulting implementation by demonstrating its application in a new problem domain fo r CBJ. (C) 2000 Elsevier Science B.V. All rights reserved.