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.
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 or by coming to my office (A07 in the Computer Science building).
If you send me an email, please put
BSc/MSc project in the subject line, so I know immediately what it is about.
