書誌事項
- 公開日
- 1993-01-02
- 権利情報
-
- https://www.acm.org/publications/policies/copyright_policy#Background
- DOI
-
- 10.1145/138027.138060
- 公開者
- Association for Computing Machinery (ACM)
この論文をさがす
説明
<jats:p> 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 <jats:italic>judgment</jats:italic> . Logics are represented in LF via a new principle, the <jats:italic>judgments as types</jats:italic> 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. </jats:p>
収録刊行物
-
- Journal of the ACM
-
Journal of the ACM 40 (1), 143-184, 1993-01-02
Association for Computing Machinery (ACM)
