A Framework for Defining Logics

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed -calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-L

• Type: Conference
• Year: 1987
• Where: LICS
• Authors: Robert Harper, Furio Honsell, Gordon D. Plotkin
• Keywords: Automated Reasoning, Edinburgh Logical Framework, Formal Systems, LICS 1987, Proof Checking