A Framework for Defining Logics This paper presents the Edinburgh Logical Framework (LF), a system for defining logics using a typed λ-calculus with dependent types. LF provides a general method for representing logics by identifying judgments with types and proofs with terms. This allows for a uniform treatment of rules and proofs, where rules are viewed as proofs of higher-order judgments. The LF type system is designed to be as weak as possible to support practical unification and matching algorithms. It includes three levels of terms: objects, types, and kinds. The system supports binding operators, schematic abstraction, and variable-occurrence conditions. The LF type system is sufficiently expressive to represent various logics, including first-order and higher-order logic. The paper discusses the metatheoretic properties of LF, including definitional equality, strong normalization, and the decidability of the type system. It also presents the theory of syntax, rules, and proofs, and discusses related work. The paper concludes with a discussion of the significance of LF in the development of logic-independent proof development environments.A Framework for Defining Logics This paper presents the Edinburgh Logical Framework (LF), a system for defining logics using a typed λ-calculus with dependent types. LF provides a general method for representing logics by identifying judgments with types and proofs with terms. This allows for a uniform treatment of rules and proofs, where rules are viewed as proofs of higher-order judgments. The LF type system is designed to be as weak as possible to support practical unification and matching algorithms. It includes three levels of terms: objects, types, and kinds. The system supports binding operators, schematic abstraction, and variable-occurrence conditions. The LF type system is sufficiently expressive to represent various logics, including first-order and higher-order logic. The paper discusses the metatheoretic properties of LF, including definitional equality, strong normalization, and the decidability of the type system. It also presents the theory of syntax, rules, and proofs, and discusses related work. The paper concludes with a discussion of the significance of LF in the development of logic-independent proof development environments.