Get 20M+ Full-Text Papers For Less Than $1.50/day. Subscribe now for You or Your Team.

Learn More →

A framework for defining logics

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-Lo¨f's system of arities. The treatment of rules and proofs focuses on his notion of a judgment . Logics are represented in LF via a new principle, the judgments as types principle, whereby each judgment is identified with the type of its proofs. This allows for a smooth treatment of discharge and variable occurence conditions and leads to a uniform treatment of rules and proofs whereby rules are viewed as proofs of higher-order judgments and proof checking is reduced to type checking. The practical benefit of our treatment of formal systems is that logic-independent tools, such as proof editors and proof checkers, can be constructed. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of the ACM (JACM) Association for Computing Machinery

Loading next page...
 
/lp/association-for-computing-machinery/a-framework-for-defining-logics-NisPxnWu8M

References

References for this paper are not available at this time. We will be adding them shortly, thank you for your patience.

Publisher
Association for Computing Machinery
Copyright
The ACM Portal is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.
ISSN
0004-5411
DOI
10.1145/138027.138060
Publisher site
See Article on Publisher Site

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-Lo¨f's system of arities. The treatment of rules and proofs focuses on his notion of a judgment . Logics are represented in LF via a new principle, the judgments as types principle, whereby each judgment is identified with the type of its proofs. This allows for a smooth treatment of discharge and variable occurence conditions and leads to a uniform treatment of rules and proofs whereby rules are viewed as proofs of higher-order judgments and proof checking is reduced to type checking. The practical benefit of our treatment of formal systems is that logic-independent tools, such as proof editors and proof checkers, can be constructed.

Journal

Journal of the ACM (JACM)Association for Computing Machinery

Published: Jan 2, 1993

References