Sciweavers

Share
CORR
2008
Springer

Reasoning in Abella about Structural Operational Semantics Specifications

8 years 2 months ago
Reasoning in Abella about Structural Operational Semantics Specifications
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.
Andrew Gacek, Dale Miller, Gopalan Nadathur
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Andrew Gacek, Dale Miller, Gopalan Nadathur
Comments (0)
books