Name
Abstract | ||
|---|---|---|
this paper and the LF. In particular theidea of having an operator T : Prop ! Type appears already in De Bruijn's earlierwork, as does the idea of having several judgements.The paper [24] describes the basic features of the LF. In this paper we are goingto provide a broader illustration of its applicability and discuss to what extent it issuccessful. The analysis (of the formal presentation) of a system carried out throughencoding often illuminates the system itself. This paper will also... |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/BF00245294 | Journal of Automated Reasoning |
Keywords | Field | DocType |
Lambda calculus,formal systems,Edinburgh Logical Framework,proof checking | Specification language,Formal system,Programming language,Non-classical logic,Typed lambda calculus,Natural deduction,Computer science,System F,Algorithm,Mathematical proof,Logical framework | Journal |
Volume | Issue | ISSN |
9 | 3 | 0168-7433 |
Citations | PageRank | References |
64 | 15.56 | 17 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Arnon Avron | 1 | 1292 | 147.65 |
| Furio Honsell | 2 | 1254 | 146.59 |
| Ian A. Mason | 3 | 797 | 97.47 |
| Robert Pollack | 4 | 64 | 15.56 |