Abella
E514254
Abella is an interactive theorem prover and proof assistant designed for reasoning about relational specifications, particularly those involving higher-order abstract syntax and inductive and coinductive definitions.
Statements (45)
| Predicate | Object |
|---|---|
| instanceOf |
interactive theorem prover
ⓘ
proof assistant ⓘ |
| appliedIn |
formalization of meta-theory of programming languages
ⓘ
verification of properties of logical frameworks ⓘ |
| basedOn | logic G ⓘ |
| canReasonAbout |
lambda-calculus
ⓘ
process calculi ⓘ type systems ⓘ |
| designedFor |
reasoning about formal systems
ⓘ
reasoning about operational semantics ⓘ reasoning about programming languages ⓘ |
| developedBy |
Alwen Tiu
NERFINISHED
ⓘ
Dale Miller NERFINISHED ⓘ Gopalan Nadathur NERFINISHED ⓘ |
| firstReleasedIn | 2000s ⓘ |
| hasFeature |
automation for routine proof steps
ⓘ
interactive proof development ⓘ support for binding and substitution reasoning ⓘ support for cut-admissibility style arguments ⓘ support for structural properties of contexts ⓘ tactic-based proof construction ⓘ |
| hasWebsite | http://abella-prover.org/ ⓘ |
| implements | two-level logic approach ⓘ |
| isFreeSoftware | true ⓘ |
| supports |
HOAS-style encodings
ⓘ
case analysis ⓘ coinduction ⓘ coinductive definitions ⓘ context reasoning ⓘ definitions by clauses ⓘ eigenvariable reasoning ⓘ equality reasoning ⓘ fixed-point definitions ⓘ generic judgments ⓘ higher-order abstract syntax ⓘ higher-order hereditary Harrop formulas ⓘ induction ⓘ inductive definitions ⓘ lambda-tree syntax ⓘ proof scripts ⓘ reasoning about relational specifications ⓘ unification over lambda-terms ⓘ |
| uses |
reasoning logic
ⓘ
specification logic ⓘ |
| writtenIn | OCaml NERFINISHED ⓘ |
Referenced by (2)
Full triples — surface form annotated when it differs from this entity's canonical label.