A Framework for Defining Logics

Robert Harper? Furio Honselly Gordon Plotkinz

Abstract

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?of's system of arities. The treatment of rules and proofs focuses on his notion of a judgement. Logics are represented in 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. The practical benefit of our treatment of formal systems is that logic-indep endent tools such as proof editors and proof checkers can be constructed.
Categories and subject descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic.
General terms: algorithms, theory, verification.
Additional key words and phrases: typed lambda calculus, formal systems, proof checking, interactive theorem proving.

1 Introduction

Much work has been devoted to building systems for checking and building formal proofs in various logical systems. Research in this area was initiated by de Bruijn in the AUTOMATH project whose purpose was to formalize mathematical arguments in a language suitable for machine checking [15]. Interactive proof construction was first considered by Milner, et. al. in the LCF system [19]. The fundamental idea was to exploit the abstract type mechanism of ML to provide a safe means of interactively building proofs in PP>=. These

?School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, USA yDipartimento di Matematica e Informatica, Universit?a di Udine, Via Zanon, 6, Udine, ItalyzLaboratory for Foundations of Computer Science, Edinburgh University, Edinburgh EH9- 3JZ, United Kingdom