A Framework for Defining Logics
Robert Harper? Furio Honselly Gordon Plotkinz
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.
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 . Interactive proof construction was first considered by Milner, et. al. in the LCF system . 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