Affordable Access

Publisher Website

Reasoning in Abella about Structural Operational Semantics Specifications

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
228
Identifiers
DOI: 10.1016/j.entcs.2008.12.118
Keywords
  • Structural Operational Semantics
  • Abella
  • λ-Tree Syntax
  • Object Language Binding
Disciplines
  • Linguistics
  • Logic

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.