Reasoning in Abella about structural operational semantics specifications

DOI10.1016/J.ENTCS.2008.12.118zbMATH Open1337.68239OpenAlexW2119790470MaRDI QIDQ2804943FDOQ2804943

Authors: Andrew Gacek, Gopalan Nadathur, Dale 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

Recommendations

• Abella: a system for reasoning about relational specifications
• A two-level logic approach to reasoning about computations
• Abella: a tutorial
• The Abella Interactive Theorem Prover (System Description)
• A conservative look at operational semantics with variable binding

zbMATH Keywords

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cites Work

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

Cited In (8)

• Nominal SOS
• The Abella Interactive Theorem Prover (System Description)
• Nominal abstraction
• Reasoning about assignments in recursive data structures
• On the role of names in reasoning about \(\lambda\)-tree syntax specifications
• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• A two-level logic approach to reasoning about computations
• Abella: a tutorial

Uses Software

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

This page was built for publication: Reasoning in Abella about structural operational semantics specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804943)