The LF logical framework codifies a methodology for representing
deductive systems, such as programming languages and logics, within a
dependently typed lambda-calculus. In this methodology, the syntactic
and deductive apparatus of a system is encoded as the canonical forms of
associated LF types; an encoding is correct (adequate) if and only if it
defines a compositional bijection between the apparatus of the deductive
system and the associated canonical forms. Given an adequate encoding,
one may establish metatheoretic properties of a deductive system by
reasoning about the associated LF representation. The Twelf
implementation of the LF logical framework is a convenient and powerful
tool for putting this methodology into practice. Twelf supports both
the representation of a deductive system and the mechanical verification
of proofs of metatheorems about it.
The purpose of this paper is to provide an up-to-date overview of the LF
lambda-calculus, the LF methodology for adequate representation, and the
Twelf methodology for mechanizing metatheory. We begin by defining a
variant of the original LF language, called Canonical LF, in which only
canonical forms (long beta-eta-normal forms) are permitted. This
variant is parameterized by a subordination relation, which enables
modular reasoning about LF representations. We then give an adequate
representation of a simply typed lambda-calculus in Canonical LF, both
to illustrate adequacy and to serve as an object of analysis. Using
this representation, we formalize and verify the proofs of some
metatheoretic results, including preservation, determinacy, and
strengthening. Each example illustrates a significant aspect of using
LF and Twelf for formalized metatheory.