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.

Symbol	Unicode	Name	Meaning
Π	U+03A0	Pi	Dependent product
λ	U+03BB	Lambda	Abstraction
Type	—	Type	Base kind
:	—	Judgment	Inhabitation
→	U+2192	Arrow	Function type
⊢	U+22A2	Derives	Derivability

Metatheory. LF has decidable type checking. Canonical forms lemma: unique representatives. Hereditary substitution: strong normalization. Adequacy proofs establish encoding correctness. Meta-reasoning: Twelf's coverage, totality checking.

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

Limitations. HOAS complicates some metatheory. Negative occurrences require care. Tool support concentrated (Twelf). Learning curve steep. Not mainstream in verification. Relating encodings to implementations takes work.