Reasoning in Abella about Structural Operational Semantics Specifications

Andrew Gacek, Dale Miller, Gopalan Nadathur

Research output: Contribution to journalArticlepeer-review

14 Scopus citations


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 languageEnglish (US)
Pages (from-to)85-100
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Issue numberC
StatePublished - 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.


  • Abella
  • Structural operational semantics
  • object language binding
  • λ-tree syntax


Dive into the research topics of 'Reasoning in Abella about Structural Operational Semantics Specifications'. Together they form a unique fingerprint.

Cite this