Abella
swMATH ID:  9461 
Software Authors:  Andrew Gacek 
Description:  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 twolevel 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. 
Homepage:  http://abellaprover.org/ 
Related Software:  Twelf; Beluga; Coq; Isabelle/HOL; PoplMark; Bedwyr; Teyjus; Nominal Isabelle; HYBRID; Agda; Isabelle; ELPI; Delphin; Ott; seL4; TPTP; Leo; Satallax; LNgen; HOL 
Referenced in:  52 Publications 
Standard Articles
2 Publications describing the Software, including 2 Publications in zbMATH  Year 

Abella: a system for reasoning about relational specifications. Zbl 1451.68315 Baelde, David; Chaudhuri, Kaustuv; Gacek, Andrew; Miller, Dale; Nadathur, Gopalan; Tiu, Alwen; Wang, Yuting 
2014

The Abella interactive theorem prover. (System description). Zbl 1165.68457 Gacek, Andrew 
2008

all
top 5
Referenced by 66 Authors
all
top 5
Referenced in 11 Serials
Referenced in 4 Fields
49  Computer science (68XX) 
26  Mathematical logic and foundations (03XX) 
1  General and overarching topics; collections (00XX) 
1  Quantum theory (81XX) 