Logical Frameworks

Origin. Harper, Honsell, Plotkin introduced LF (Edinburgh Logical Framework, 1993). Meta-languages for defining logics. Represent syntax, judgments, and derivations. Encode object logics faithfully. Foundation for Twelf, Beluga, and other systems.

Models. Meta-logic for specifying logics. Define syntax with binding (HOAS). Define judgments as type families. Derivations as terms: "proofs as programs." Adequacy: encoding bijectively represents object logic. Mechanized metatheory.

Formalism.

LF type theory: Kinds: Type, Πx:A. K Types: a | A → B | Πx:A. B Terms: x | c | λx:A.M | M N

Dependent types: Πx:A. B — type B depends on term x:A. Enables encoding of binding and judgments.

Higher-Order Abstract Syntax (HOAS): Object-level binding = meta-level λ. lam: (tm → tm) → tm Substitution handled by meta-level β-reduction.

Judgments as types: of : tm → tp → Type (typing judgment) Derivation d : of M T represents proof that M : T.

Example (simply-typed λ-calculus): tp : Type. arr : tp → tp → tp. tm : Type. lam : tp → (tm → tm) → tm. app : tm → tm → tm. of : tm → tp → Type. of_lam : ({x:tm} of x T1 → of (M x) T2) → of (lam T1 M) (arr T1 T2). of_app : of M (arr T1 T2) → of N T1 → of (app M N) T2.

Adequacy: Bijection between LF terms and object-logic derivations. Full, faithful encoding.

Symbols.

Metatheory. LF is the dependently typed λ-calculus λΠ, and its metatheory is what makes it usable as a framework: it is strongly normalizing, βη-conversion is decidable, and therefore type checking is decidable. Harper and Pfenning (2005) recast these results without appeal to normalization of arbitrary terms, giving a type-directed algorithmic equality, and Watkins, Cervesato, Pfenning and Walker (2003) introduced hereditary substitution — substitution that contracts the redexes it creates as it goes — so that canonical forms exist and are unique. The canonical forms lemma is the engine of adequacy: an encoding is adequate when there is a compositional bijection between the canonical LF terms of a type and the derivations of the object logic, one that commutes with substitution. Adequacy has to be proved for each encoding; the framework does not supply it. Twelf's totality checking — mode, termination and coverage — turns a relation into a checked meta-theorem, and it operates on an LF signature from outside rather than within LF.

Applies to. Proof assistant design. Mechanized metatheory. Language specification. Compiler verification. Type system specification. Logic education. Proof carrying code.

Limitations. LF represents derivations; it does not reason about them. There is no induction principle over LF types inside LF, so every meta-theorem must be established in an external meta-logic — which is what Twelf's totality checker is — and coverage checking is undecidable, so the checker is conservative and rejects some total relations. Higher-order abstract syntax is the second limit. A constructor such as lam : (tm → tm) → tm places tm negatively, so tm is not an inductive type and the encoding cannot be transplanted into Coq or Agda without auxiliary well-formedness predicates. Adequacy is a paper theorem about the gap between an object logic and its signature, and nothing machine-checks it. LF's equality is βη only, so object-level computation has to be encoded as a judgment rather than run.

© 2026 Lingenic LLC