A Framework for Defining Logics

R. Harper, F. Honsell and G. Plotkin

Abstract: The Logical Framework (LF) is a system for defining a wide class of logics. It is based on a general treatment of syntax, rules, and proofs in terms of a typed lambda-calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-Lof's system of arities. The treatment of rules and proofs focuses on the notion of a judgement. Logics are encoded in the LF via a new principle, the judgements as types principle, whereby each judgement is identified with the type of its proofs. This allows for a smooth treatment of discharge and variable occurrence conditions and leads to a uniform treatment of rules and proofs whereby rules are viewed as proofs of higher-order judgements and proof checking is reduced to type checking. An important benefit of our treatment of formal systems is that logic-independent tools such as proof editors and proof checkers can be constructed.

LFCS report ECS-LFCS-87-23

This report was published in Journal of the ACM vol.40, no. 1 (Jan. 1993) pp. 143-184.

Previous | Index | Next