  We describe the development of a logic for reasoning about specifications in
the Edinburgh Logical Framework (LF). In this logic, typing judgments in LF
serve as atomic formulas, and quantification is permitted over contexts and
terms that might appear in them. Further, contexts, which constitute type
assignments to uniquely named variables that are modeled using the technical
device of nominal constants, can be characterized via an inductive description
of their structure. We present a semantics for such formulas and then consider
the task of proving them. Towards this end, we restrict the collection of
formulas we consider so as to ensure that they have normal forms upon which
proof rules may be based. We then specifically discuss a proof rule that
provides the basis for case analysis over LF typing judgments; this rule is the
most complex and innovative one in the collection. We illustrate the proof
system through an example. Finally, we discuss ongoing work and we relate our
project to existing systems that have a similar goal.
