Abella: A System for Reasoning about Relational Specifications

DOI10.6092/issn.1972-5787/4650zbMath1451.68315OpenAlexW1961757151MaRDI QIDQ5195258

Gopalan Nadathur, Kaustuv Chaudhuri, David Baelde, Alwen Tiu, Andrew Gacek, Yu-Ting Wang, Dale A. Miller

Publication date: 18 September 2019

Full work available at URL: https://hal.inria.fr/hal-01102709

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Functions-as-constructors higher-order unification: extended pattern unification, The undecidability of proof search when equality is a logical connective, Proof checking and logic programming, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, A Survey of the Proof-Theoretic Foundations of Logic Programming, Constraint handling rules with binders, patterns and generic quantification, Towards substructural property-based testing, Rensets and renaming-based recursion for syntax with bindings extended version, Formalized meta-theory of sequent calculi for linear logics, A strong call-by-need calculus, A formalized general theory of syntax with bindings: extended version, Formalized meta-theory of sequent calculi for substructural logics, \(\mathrm{HO}\pi\) in Coq, Proof-relevant π-calculus: a constructive account of concurrency and causality, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, On the effectiveness of higher-order logic programming in language-oriented programming, Unnamed Item, Subformula linking for intuitionistic logic with application to type theory, Abella, Implementing type theory in higher order constraint logic programming, A case study in programming coinductive proofs: Howe’s method, Mechanized metatheory revisited, Divergence and unique solution of equations, Rensets and renaming-based recursion for syntax with bindings