Abella: A System for Reasoning about Relational Specifications
The Abella interactive theorem prover is based on an intuitionistic logic that allows for inductive and co-inductive reasoning over relations. Abella supports the λ-tree approach to treating syntax containing binders: it allows simply typed λ-terms to be used to represent such syntax and it provides...
| Main Authors: | , , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2014-12-01
|
| Series: | Journal of Formalized Reasoning |
| Online Access: | http://jfr.unibo.it/article/view/4650 |