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.


References in zbMATH (referenced in 52 articles , 2 standard articles )

Showing results 21 to 40 of 52.
Sorted by year (citations)
  1. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification (2016)
  2. Wang, Yuting; Nadathur, Gopalan: A higher-order abstract syntax approach to verified transformations on functional programs (2016)
  3. Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
  4. Miller, Dale: Proof checking and logic programming (2015)
  5. Olarte, Carlos; Pimentel, Elaine: Proving concurrent constraint programming correct, revisited (2015)
  6. Pientka, Brigitte; Cave, Andrew: Inductive beluga: programming proofs (2015)
  7. Steen, Alexander; Benzmüller, Christoph: There is no best (\beta)-normalization strategy for higher-order reasoners (2015)
  8. Wisniewski, Max; Steen, Alexander; Benzmüller, Christoph: \textscLeoPARD-- a generic platform for the implementation of higher-order reasoners (2015)
  9. Baelde, David; Chaudhuri, Kaustuv; Gacek, Andrew; Miller, Dale; Nadathur, Gopalan; Tiu, Alwen; Wang, Yuting: Abella: a system for reasoning about relational specifications (2014)
  10. Southern, Mary; Chaudhuri, Kaustuv: A two-level logic approach to reasoning about typed specification languages (2014)
  11. Savary-Belanger, Olivier; Monnier, Stefan; Pientka, Brigitte: Programming type-safe transformations using higher-order abstract syntax (2013)
  12. Accattoli, Beniamino: Proof pearl: Abella formalization of (\lambda)-calculus cube property (2012)
  13. Cimini, Matteo; Mousavi, Mohamamdreza; Reniers, Michel A.; Gabbay, Murdoch J.: Nominal SOS (2012)
  14. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  15. Gacek, Andrew: Abella: a tutorial (2012)
  16. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  17. Lee, Gyesik; Oliveira, Bruno C. D. S.; Cho, Sungkeun; Yi, Kwangkeun: GMeta: a generic formal metatheory framework for first-order representations (2012)
  18. Cheney, James; Urban, Christian: Mechanizing the metatheory of mini-XQuery (2011)
  19. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Nominal abstraction (2011)
  20. Dawson, Jeremy E.; Goré, Rajeev: Generic methods for formalising sequent calculi applied to provability logic (2010)