Amy Felty and Dale Miller. In

**Abstract:**
Various forms of typed lambda-calculi have been proposed as
specification languages for representing wide varieties of object
logics. The *logical framework*, LF, is an example of such a
dependent-type lambda-calculus. A small subset of intuitionistic
logic with quantification over simply typed lambda-calculus has also
been proposed as a framework for specifying general logics. The logic
of *hereditary Harrop* formulas with quantification at all
non-predicate types, denoted here as *hh-omega*, is such a
meta-logic that has been implemented in both the Isabelle theorem
prover and the lambda Prolog logic programming language. Both
frameworks provide for specifications of logics in which details
involved with free and bound variable occurrences, substitutions,
eigenvariables, and the scope of assumptions within object logics are
handled correctly and elegantly at the "meta" level. In this paper,
we show how LF can be encoded into *hh-omega* in a direct and
natural way by mapping the typing judgments in LF into propositions in
the logic of *hh-omega*. This translation establishes a very
strong connection between these two languages: the order of
quantification in an LF signature is exactly the order of a set of
*hh-omega* clauses, and the proofs in one system correspond
directly to proofs in the other system. Relating these two languages
makes it possible to provide implementations of proof checkers and
theorem provers for logics specified in LF by using standard logic
programming techniques which can be used to implement *hh-omega*.