登入
選單
返回
Google圖書搜尋
A Framework for Defining Logics
Robert Harper
Furio Honsell
University of Edinburgh. Laboratory for Foundations of Computer Science
Gordon Plotkin
出版
LFCS, Department of Computer Science, University of Edinburgh
, 1991
URL
http://books.google.com.hk/books?id=Am7eJAAACAAJ&hl=&source=gbs_api
註釋
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 [lambda]-calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-Löf'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.
