×

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 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.
Homepage: http://abella-prover.org/
Related Software: Twelf; Beluga; Coq; Isabelle/HOL; PoplMark; Bedwyr; Teyjus; Nominal Isabelle; HYBRID; Agda; Isabelle; ELPI; Delphin; Ott; seL4; Tac; Freshml; HOL; TPTP; Leo
Cited in: 53 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

Cited by 66 Authors

9 Pientka, Brigitte
7 Miller, Dale Allen
6 Gacek, Andrew
5 Nadathur, Gopalan
4 Chaudhuri, Kaustuv
4 Felty, Amy P.
3 Cimini, Matteo
3 Momigliano, Alberto
3 Tiu, Alwen Fernanto
2 Baelde, David
2 Benzmüller, Christoph Ewald
2 Cheney, James
2 Libal, Tomer
2 Oliveira, Bruno C.d. S.
2 Reis, Giselle
2 Steen, Alexander
2 Wang, Yuting
1 Accattoli, Beniamino
1 Ahn, Ki Yung
1 Ambal, Guillaume
1 Armando, Alessandro
1 Baumgartner, Peter
1 Cave, Andrew
1 Cho, Sungkeun
1 Dawson, Jeremy E.
1 Dowek, Gilles
1 Dunfield, Joshua
1 Errington, Jacob
1 Gabbay, Murdoch James
1 Gheri, Lorenzo
1 Goré, Rajeev Prabhakar
1 Goubault-Larrecq, Jean
1 Guidi, Ferruccio
1 Hage, Jurriaan
1 Horne, Ross
1 Jang, Junyoung
1 Kaiser, Jonas Pilgaard
1 Lee, Gyesik
1 Lenglet, Sergueï
1 Mahmoud, Mohamed Yousri
1 Monnier, Stefan
1 Mousavi, Mohamamdreza
1 Olarte, Carlos
1 Perera, Roly
1 Pimentel, Elaine
1 Rabe, Florian
1 Reniers, Michel Adriaan
1 Sacerdoti Coen, Claudio
1 Savary-Belanger, Olivier
1 Schack-Nielsen, Anders
1 Schmitt, Alan
1 Schrijvers, Tom
1 Schürmann, Carsten
1 Serrano, Alejandro
1 Siek, Jeremy G.
1 Smolka, Gert
1 Snow, Zachary
1 Southern, Mary
1 Straßburger, Lutz
1 Tassi, Enrico
1 Thibodeau, David
1 Urban, Christian
1 Viel, Alexandre
1 Wisniewski, Max
1 Yi, Kwangkeun
1 Zhao, Jinxu
all top 5

Cited in 11 Serials

7 Journal of Automated Reasoning
4 MSCS. Mathematical Structures in Computer Science
2 Annals of Mathematics and Artificial Intelligence
1 Theoretical Computer Science
1 Information and Computation
1 Formal Aspects of Computing
1 Theory and Practice of Logic Programming
1 ACM Transactions on Computational Logic
1 Lecture Notes in Computer Science
1 Journal of Formalized Reasoning
1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences

Cited in 4 Fields

50 Computer science (68-XX)
26 Mathematical logic and foundations (03-XX)
1 General and overarching topics; collections (00-XX)
1 Quantum theory (81-XX)

Citations by Year