Computer Science – Logic in Computer Science
Scientific paper
2008-04-24
Computer Science
Logic in Computer Science
15 pages. To appear in LFMTP'08
Scientific paper
The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses lambda 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.
Gacek Andrew
Miller Daniel D.
Nadathur Gopalan
No associations
LandOfFree
Reasoning in Abella about Structural Operational Semantics Specifications does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Reasoning in Abella about Structural Operational Semantics Specifications, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Reasoning in Abella about Structural Operational Semantics Specifications will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-505467