The Edinburgh Logical Framework (LF) is a framework for defining and presenting logics using a typed λ-calculus with dependent types. It treats syntax similarly to Martin-Löf's system but with more generality, focusing on the concept of judgments. Logics are represented in LF through the "judgments as types" principle, where each judgment is identified with the type of its proofs. This allows for a uniform treatment of rules and proofs, reducing proof checking to type checking. The framework supports logic-independent tools like proof editors and checkers. The LF type theory is based on a predicative, dependently-typed λ-calculus, closely related to AUTOMATH languages. It includes three levels of terms: objects, types, and kinds, with definitional equality playing a central role. The framework ensures decidability of the type system, which is crucial for reducing proof checking to type checking. The paper also discusses the representation of syntax and the treatment of rules and proofs in first-order and higher-order logic, providing detailed examples and theorems to support its claims.The Edinburgh Logical Framework (LF) is a framework for defining and presenting logics using a typed λ-calculus with dependent types. It treats syntax similarly to Martin-Löf's system but with more generality, focusing on the concept of judgments. Logics are represented in LF through the "judgments as types" principle, where each judgment is identified with the type of its proofs. This allows for a uniform treatment of rules and proofs, reducing proof checking to type checking. The framework supports logic-independent tools like proof editors and checkers. The LF type theory is based on a predicative, dependently-typed λ-calculus, closely related to AUTOMATH languages. It includes three levels of terms: objects, types, and kinds, with definitional equality playing a central role. The framework ensures decidability of the type system, which is crucial for reducing proof checking to type checking. The paper also discusses the representation of syntax and the treatment of rules and proofs in first-order and higher-order logic, providing detailed examples and theorems to support its claims.