Abella
The Abella Interactive Theorem Prover (System Description). Abella [3] is an interactive system for reasoning about aspects of object languages that have been formally presented through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach to specification and reasoning. One level is defined by a specification logic which supports a transparent encoding of structural semantics rules and also enables their execution. The second level, called the reasoning logic, embeds the specification logic and allows the development of proofs of properties about specifications. An important characteristic of both logics is that they exploit the λ-tree syntax approach to treating binding in object languages. Amongst other things, Abella has been used to prove normalizability properties of the λ-calculus, cut admissibility for a sequent calculus and type uniqueness and subject reduction properties. This paper discusses the logical foundations of Abella, outlines the style of theorem proving that it supports and finally describes some of its recent applications.
Keywords for this software
References in zbMATH (referenced in 48 articles , 2 standard articles )
Showing results 1 to 20 of 48.
Sorted by year (- Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
- Chaudhuri, Kaustuv; Lima, Leonardo; Reis, Giselle: Formalized meta-theory of sequent calculi for linear logics (2019)
- Goubault-Larrecq, Jean: A semantics for nabla (2019)
- Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico: Implementing type theory in higher order constraint logic programming (2019)
- Mahmoud, Mohamed Yousri; Felty, Amy P.: Formalization of metatheory of the quipper quantum programming language in a linear logic (2019)
- Miller, Dale: Mechanized metatheory Revisited (2019)
- Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David: A case study in programming coinductive proofs: Howe’s method (2019)
- Straßburger, Lutz: The problem of proof identity, and why computer scientists should care about Hilbert’s 24th problem (2019)
- Perera, Roly; Cheney, James: Proof-relevant (\pi)-calculus: a constructive account of concurrency and causality (2018)
- Rabe, Florian: A modular type reconstruction algorithm (2018)
- Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom: Formalization of a polymorphic subtyping algorithm (2018)
- Chaudhuri, Kaustuv; Lima, Leonardo; Reis, Giselle: Formalized meta-theory of sequent calculi for substructural logics (2017)
- Cimini, Matteo; Siek, Jeremy G.: Automatically generating the dynamic semantics of gradually typed languages (2017)
- Kaiser, Jonas; Pientka, Brigitte; Smolka, Gert: Relating system F and (\lambda2): a case study in Coq, Abella and Beluga (2017)
- Miller, Dale: Proof checking and logic programming (2017)
- Serrano, Alejandro; Hage, Jurriaan: Constraint handling rules with binders, patterns and generic quantification (2017)
- Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification (2016)
- Wang, Yuting; Nadathur, Gopalan: A higher-order abstract syntax approach to verified transformations on functional programs (2016)
- Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
- Miller, Dale: Proof checking and logic programming (2015)