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 41 to 52 of 52.
Sorted by year (citations)
  1. Felty, Amy; Pientka, Brigitte: Reasoning with higher-order abstract syntax and contexts: a comparison (2010)
  2. Pientka, Brigitte: Programming inductive proofs. A new approach based on contextual types (2010)
  3. Pientka, Brigitte; Dunfield, Joshua: Beluga: a framework for programming and reasoning with deductive systems (system description) (2010)
  4. Schack-Nielsen, Anders; Schürmann, Carsten: Curry-style explicit substitutions for the linear and affine lambda calculus (2010)
  5. Snow, Zachary: Realizing the dependently typed (\lambda)-calculus (2010)
  6. Baelde, David: On the expressivity of minimal generic quantification (2009)
  7. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Reasoning in Abella about structural operational semantics specifications (2009)
  8. Tiu, Alwen: On the role of names in reasoning about (\lambda)-tree syntax specifications (2009)
  9. Armando, Alessandro (ed.); Baumgartner, Peter (ed.); Dowek, Gilles (ed.): Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings (2008)
  10. Gacek, Andrew: System description: Abella -- A system for reasoning about computations (2008) ioport
  11. Gacek, Andrew: The Abella interactive theorem prover. (System description) (2008)
  12. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Reasoning in abella about structural operational semantics specifications (2008) ioport