The Abella Interactive Theorem Prover (System Description)
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 3870635
- The Matita interactive theorem prover
- Interactive theorem proving. Preface of the special issue
- Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
- Interactive theorem proving from the perspective of Isabelle/Isar
- A synthesis of the procedural and declarative styles of interactive theorem proving
- A survey of interactive theorem proving
- Theo: An interactive proof development system
- scientific article; zbMATH DE number 1949621
- The Theorema Environment for Interactive Proof Development
Cites work
- A logic for reasoning about generic judgments
- A proof theory for generic judgments
- Automated Deduction – CADE-20
- scientific article; zbMATH DE number 1696799 (Why is no real title available?)
- Intensional interpretations of functionals of finite type I
- Logic Programming
- Reasoning in Abella about structural operational semantics specifications
- Reasoning with higher-order abstract syntax in a logical framework
- The Abella Interactive Theorem Prover (System Description)
- Theorem Proving in Higher Order Logics
- Uniform proofs as a foundation for logic programming
Cited in
(32)- TWAM: a certifying abstract machine for logic programs
- Harpoon: mechanizing metatheory interactively
- Abella
- Mechanized metatheory revisited
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- A two-level logic approach to reasoning about computations
- 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
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Abella: a tutorial
- A two-level logic approach to reasoning about typed specification languages
- Programming inductive proofs. A new approach based on contextual types
- Mechanizing the metatheory of mini-XQuery
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- Inductive beluga: programming proofs
- The Abella Interactive Theorem Prover (System Description)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- scientific article; zbMATH DE number 2003156 (Why is no real title available?)
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Abella: a system for reasoning about relational specifications
- A semantics for nabla
- 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)
- Nominal abstraction
- Mechanized metatheory revisited: an extended abstract (invited paper)
- An improved implementation and abstract interface for Hybrid
- A case study on logical relations using contextual types
- An open challenge problem repository for systems supporting binders
- Rapid prototyping formal systems in MMT: 5 case studies
- Barendregt's theory of the -calculus, refreshed and formalized
This page was built for publication: The Abella Interactive Theorem Prover (System Description)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3541698)
