Opened 12 years ago
#7 new talk request
Abella theorem prover
Reported by: | Ben Lippmeier | Owned by: | |
---|---|---|---|
Keywords: | Cc: |
Description
Abella is an interactive theorem prover based on lambda-tree syntax. This means that Abella is well-suited for reasoning about the meta-theory of programming languages and other logical systems which manipulate objects with binding.
Note: See
TracTickets for help on using
tickets.