A theorem prover “reasonEq” , written in Haskell, is currently under development. It is intended to support reasoning about the meaning and correctness of programs. It supports an easy to use proof style for predicate calculus known as “equational reasoning” – very similar to the kind of algebraic reasoning used in most mathematics found in undergraduate courses. It currently has a command-line/REPL style user interface, and a prototype GUI.
It’s hosted on Github: https://github.com/andrewbutterfield/reasonEq
Project ideas include:
- Using the prover to build a useful library of theories, as well as giving feedback on features and user interface.
- Extending the prover by adding in proof automation function to try various strategies to find proofs.
- Improving the language used to write theories.
- Improving the display of theorems and proofs.
Projects can be scoped for both 4th year projects and year 5 dissertations