student project image

School of Computer Science
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB, UK

T: +44(0) 115 9514251
F: +44(0) 115 9514254
E: csit-enquiries@cs.nott.ac.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.

Natural Deduction Prover

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.

Mathematical Games

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.

Ashta Chamma
Brax (Jinx)
Dominoes

Dependent Typed Programming and Proving

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.

Hoare Logic

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.

Contacting me

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.