Encoding the calculus of constructions in a higher-order logic

We present an encoding of the calculus of construc-tions (CC) in a higher-order intuitionistic logic (I) in a direct way, so that correct typing in CC corre-sponds to intuitionistic provability in a sequent calcu-lus for I. In addition, we demonstrate a direct corre-spondence between proofs in these two systems. The logic I is an extension of hereditary Harrop formu-las (hh) which serve as the logical foundation of the logic programming language Prolog. Like hh, I has the uniform proof property, which allows a complete non-deterministic search procedure to be described in a straightforward manner. Via the encoding, this search procedure provides a goal directed description of proof checking and proof search in CC.