The Abella Interactive Theorem Prover (System Description)

DOI10.1007/978-3-540-71070-7_13zbMath1165.68457OpenAlexW1568176286MaRDI QIDQ3541698

Andrew Gacek

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_13

Mathematics Subject Classification ID

Related Items

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ TWAM: a certifying abstract machine for logic programs ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Inductive Beluga: Programming Proofs ⋮ A two-level logic approach to reasoning about computations ⋮ Nominal abstraction ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ The Abella Interactive Theorem Prover (System Description) ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Proving concurrent constraint programming correct, revisited ⋮ Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus ⋮ Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) ⋮ Programming Inductive Proofs ⋮ On the Expressivity of Minimal Generic Quantification ⋮ Reasoning in Abella about Structural Operational Semantics Specifications ⋮ On the Role of Names in Reasoning about λ-tree Syntax Specifications ⋮ Harpoon: mechanizing metatheory interactively ⋮ Abella ⋮ Mechanizing the Metatheory of mini-XQuery ⋮ A semantics for nabla ⋮ Mechanized metatheory revisited ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic

Uses Software

• Isabelle/HOL
• Twelf

Cites Work

• Unnamed Item
• Unnamed Item
• Uniform proofs as a foundation for logic programming
• Reasoning in Abella about Structural Operational Semantics Specifications
• The Abella Interactive Theorem Prover (System Description)
• A proof theory for generic judgments
• Automated Deduction – CADE-20
• Logic Programming
• Theorem Proving in Higher Order Logics
• Intensional interpretations of functionals of finite type I
• Reasoning with higher-order abstract syntax in a logical framework
• Least and Greatest Fixed Points in Linear Logic

This page was built for publication: The Abella Interactive Theorem Prover (System Description)