  We present a system called Adelfa that provides mechanized support for
reasoning about specifications developed in the Edinburgh Logical Framework or
LF. Underlying Adelfa is a new logic named L_LF. Typing judgements in LF are
represented by atomic formulas in L_LF and quantification is permitted over
contexts and terms that appear in such formulas. Contexts, which constitute
type assignments to uniquely named variables that are modelled using the
technical device of nominal constants, are characterized in L_LF by context
schemas that describe their inductive structure. We present these formulas and
an associated semantics before sketching a proof system for constructing
arguments that are sound with respect to the semantics. We then outline the
realization of this proof system in Adelfa and illustrate its use through a few
example proof developments. We conclude the paper by relating Adelfa to
existing systems for reasoning about LF specifications.
