Suggestions for BSc and MSc projects
Below you can find some suggestions for student projects.
Computer-checked proofs of results in mathematics and computer science
This project is suitable for students with an interest in logic and formal proofs.
Computer proof assistants are computer programmes that check the correctness of mathematical proofs. For this to work, the proofs, and the results that they prove, have to be written in a formal language that can be understood by a computer.
Computer proof assistants can, in principle, check results in any area of endeavour, as long as these results are the product of rigorous logical reasoning. However, so far they have predominantly been used to check results in mathematics and computer science.
An important example of a computer-checked proof in mathematics is the Kepler Conjecture from the 17th century.
A computer-checked proof of this conjecture was presented in the year 2017.
Many different computer proof assistants exist, based on various different logics.
In this project, we propose formulating and proving some result – to be chosen in accordance with the interests of the student – of mathematics or computer science in a suitable computer proof assistant. Such a result could be, e.g.:
- The correctness of a sorting algorithm, i.e., programming the algorithm and showing that the output of the algorithm is always sorted.
- Error-correction properties of linear codes. This project involves implementing matrices and operations on them, as well as proving correctness of those operations.
A tool to build certified natural deduction proofs via drag-and-drop
This project is suitable for students with an interest in logic and GUI programming.
Natural deduction proofs for propositional logic are tree-shaped derivations built from basic building blocks called inference rules.
Such proofs are shown, e.g., in this course.
This project consists in building a tool that allows to build proof trees by drag-and-drop. The programme should check that only valid proofs can be built, and reject invalid (ill-formed) proof trees.
A type checker for (directed) type theory
Difficult This project is suitable for students with an interest in dependent type theory and functional programming.
Computer proof assistants mechanically check the correctness of mathematical proofs written in a formal language. Two such computer proof assistants are Agda and Coq. They are based on type theory; type theory is a strongly typed (functional) programming language similar to Haskell or Ocaml.
The core of these computer proof assistants is a type checker. A type checker takes, as an input, two terms t and T and check whether “t : T” (read: t is of type T) holds. A type checker is often accompanied by a type inferrer: a function that, given a term t, returns a term T such that “t : T” holds (type synthesis).
A project could consist in writing a type checker for type theory.
Even more difficult In a recent work (click here), Riehl and Shulman present a directed type theory, a powerful, but complicated generalization of type theory. One could attempt to write a type-checker for this directed type theory. This type checker could form the core of a proof checker for directed type theory.