The Edinburgh Logical Framework (LF) provides a means to define (or present)
logics.  It is based on a general treatment of syntax, rules, and proofs by
means of a typed $\lambda$-calculus with dependent types.  Syntax is treated
in a style similar to, but more general than, Martin-L\"of's system of
arities.  The treatment of rules and proofs focuses on his notion of a {\em
judgement}.  Logics are represented in LF via a new principle, the {\em
judgements as types} principle, whereby each judgement is identified with the
type of its proofs.  This allows for a smooth treatment of discharge and
variable occurrence conditions and leads to a uniform treatment of rules and
proofs whereby rules are viewed as proofs of higher-order judgements and proof
checking is reduced to type checking.  The practical benefit of our treatment
of formal systems is that logic-independent tools such as proof editors and
proof checkers can be constructed.