  Dependently typed lambda calculi such as the Edinburgh Logical Framework (LF)
are a popular means for encoding rule-based specifications concerning formal
syntactic objects. In these frameworks, relations over terms representing
formal objects are naturally captured by making use of the dependent structure
of types. We consider here the meaning-preserving translation of specifications
written in this style into a predicate logic over simply typed {\lambda}-terms.
Such a translation can provide the basis for efficient implementation and
sophisticated capabilities for reasoning about specifications. We start with a
previously described translation of LF specifications to formulas in the logic
of higher-order hereditary Harrop (hohh) formulas. We show how this translation
can be improved by recognizing and eliminating redundant type checking
information contained in it. This benefits both the clarity of translated
formulas, and reduces the effort which must be spent on type checking during
execution. To allow this translation to be used to execute LF specifications,
we describe an inverse transformation from hohh terms to LF expressions; thus
computations can be carried out using the translated form and the results can
then be exported back into LF. Execution based on LF specifications may also
involve some forms of type reconstruction. We discuss the possibility of
supporting such a capability using the translation under some reasonable
restrictions on the structure of specifications.
