Name
Abstract | ||
|---|---|---|
Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. We provide these capabilities here by using a logic called ${\cal G}$ which represents relations over 驴-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. We show how provability in the specification logic can be transparently encoded in ${\cal G}$ . We also describe an interactive theorem prover called Abella that implements ${\cal G}$ and this two-level logic approach and we present several examples that demonstrate the efficacy of Abella in reasoning about computations. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/s10817-011-9218-1 | Journal of Automated Reasoning |
Keywords | DocType | Volume |
Two-level logic,Nominal abstraction,Generic judgments,∇-quantification,λ,-tree syntax | Journal | 49 |
Issue | ISSN | Citations |
2 | 0168-7433 | 25 |
PageRank | References | Authors |
0.92 | 32 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrew Gacek | 1 | 252 | 16.87 |
| Dale Miller | 2 | 90 | 5.17 |
| Gopalan Nadathur | 3 | 1047 | 117.85 |