Reasoning in Abella about Structural Operational Semantics Specifications

TL;DR

This paper discusses how the Abella system supports reasoning about structural operational semantics specifications using lambda tree syntax, recursive definitions, and generic judgments, with practical demonstrations and comparisons.

Contribution

It introduces a method for reasoning about operational semantics in Abella, integrating lambda tree syntax and recursive definitions to handle binding and properties explicitly.

Findings

Effective reasoning about binding properties demonstrated

Recursive definitions enhance expressiveness in Abella

Comparisons show advantages over other logic approaches

Abstract

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.