Abstract
The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses λ-tree syntax to treat object language binding and encodes binding related properties in generic judgments. Further, object language specifications are embedded directly into the reasoning framework through recursive definitions. The treatment of binding via generic judgments implicitly enforces distinctness and atomicity in the names used for bound variables. These properties must, however, be made explicit in reasoning tasks. This objective can be achieved by allowing recursive definitions to also specify generic properties of atomic predicates. The utility of these various logical features in the Abella system is demonstrated through actual reasoning tasks. Brief comparisons with a few other logic based approaches are also made.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 85-100 |
| Number of pages | 16 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 228 |
| Issue number | C |
| DOIs | |
| State | Published - Jan 5 2009 |
Bibliographical note
Funding Information:1 Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN 55455. 2 INRIA Saclay -ˆIle-de-France & LIX/École polytechnique, Palaiseau, France 3 This work has been supported by INRIA through the “Equipes Associées” Slimmer, and by the NSF Grant CCR-0429572 which includes funding for Slimmer. Opinions, findings, and conclusions or recommendations expressed in this papers are those of the authors and do not necessarily reflect the views of the National Science Foundation.
Keywords
- Abella
- Structural operational semantics
- object language binding
- λ-tree syntax