Give a semantics to a programming language you like, or a programming paradigm, as you've studied in "Semantics and Correctness" (IBC026) or "Semantics and Rewriting" (IBC025). Example are: the bachelor theses of Tom Nikken who studied iTasks, supervised by Peter Achten and Herman Geuvers, and Janne van den Hout who studied continuations in functional languages. This can also be done as an MSc project, notably when you have studied the Master course "Semantics and Domain Theory" (IMC011).
Contact: Herman Geuvers
There is (a lot of) work on this by, for example, van Leeuwen - Wiederman, Baeten - Luttik van Tilburg, Wegner, Goldin, Smolka and many others. Many questions on the universality of these models and their relative strength remain. A bachelor thesis on this topic has been written by Rick Erkens, but there is still a lot to be studied!
Contact: Herman Geuvers
Termination of term rewriting systems is an undecidable problem in principle. However, there are many techniques that can prove termination or non-termination in some cases. In this project, you will develop methods to prove termination of many-sorted term rewriting systems (essentially: term rewriting systems where terms must be well-typed) and implement them in a fully automatic tool. For this, you will both adapt existing methods for rewriting without types, and develop your own methods specific to many-sorted term rewriting.
Contact: Cynthia Kop