Reasoning in Abella about structural operational semantics specifications

DOI10.1016/J.ENTCS.2008.12.118MaRDI QIDQ2804943zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(9)

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

Describes a project that uses

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)