School of Computer Science

University of Nottingham

Jubilee Campus, Wollaton Road

Nottingham NG8 1BB, UK

Here are a few ideas for individual projects both for BSc and MSc students. You can also come to me with your own idea for a project in a topic related to these subject areas. In general, I suggest that you use Haskell as the programming language to develop your software, since these problems are more easily solved with a functional programming language. In some of the projects, you are also required to use a proof assistant like Coq or Agda. If you prefer to use other programming languages and tools, you have to make a good case of why you think they are more suitable for the task that you chose.

Develop an implementation of propositional (or, more advanced, predicate) logic. Build an interactive system in which the user can develop derivations in Fitch-style natural deduction. For a more ambitious project: develop an automatic prover for propositional logic or a AI-based prover for predicate logic.

Implement a finite, complete-information, two-players game of the kind studied in *Winning Ways for your Mathematical Plays* by Berlekamp, Conway and Guy. Your implementation must allow two users to play against each other and also against the computer. If the game has a feasible winning strategy, implement it, otherwise use some AI technique.
The interface can be a simple, ASCII-based representation or you may develop a nicer-looking graphical environment.

Use a dependently typed programming language / proof assistant (Coq or Agda) to implement some interesting algorithm on discrete data structures (for example some famous graph algorithm) and then use the logical system to prove the correctness of your implementation.

Use Agda or Coq to implement the rules of Hoare Logic (from the module *Derivation of Algorithms*) to prove the correctness of imperative programs with respect to a specification.

Please don't hesitate to ask me any question you may have about the projects.
You can contact me by e-mail: put *Student Project* in the subject line, so I know immediately that it is about this module.