Reasoning in Abella about Structural Operational Semantics Specifications

DOI10.1016/j.entcs.2008.12.118zbMath1337.68239OpenAlexW2119790470MaRDI QIDQ2804943

Andrew Gacek, Gopalan Nadathur, Dale A. Miller

Publication date: 6 May 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.118

zbMATH Keywords

structural operational semanticsAbella\(\lambda\)-tree syntaxobject language binding

Mathematics Subject Classification ID

Related Items (5)

Nominal SOS ⋮ Nominal abstraction ⋮ The Abella Interactive Theorem Prover (System Description) ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ On the Role of Names in Reasoning about λ-tree Syntax Specifications

Uses Software

• Coq
• Isabelle/HOL
• Twelf
• Bedwyr
• Abella
• Nominal Isabelle
• Teyjus
• Lolli

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Forum: A multiple-conclusion specification logic
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Unification under a mixed prefix
• Logic programming in a fragment of intuitionistic linear logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Uniform proofs as a foundation for logic programming
• Engineering formal metatheory
• The Abella Interactive Theorem Prover (System Description)
• A framework for defining logics
• A proof theory for generic judgments
• Automated Deduction – CADE-20
• Intensional interpretations of functionals of finite type I
• Reasoning with higher-order abstract syntax in a logical framework

This page was built for publication: Reasoning in Abella about Structural Operational Semantics Specifications