print · source · login   

Theme: Foundations

Operational Semantics and/or Axiomatics Semantics for programming languages or programming paradigms (BaSc, MSc)

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

Extensions of the Turing machine or lambda calculus paradigm with interaction, advice or oracles (BaSc, MSc)

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

Complexity of puzzles and games (BSc)

For several puzzles one can wonder how hard they are to solve. A standard level of hardness is NP-completeness, and for many puzzles one can prove they are NP-complete. Coming up with a puzzle of your own choice and investigate its complexity class is a nice topic for a bachelor project. Similarly, one may investigate whether some configuration in a particular game has a winning strategy. Since 2017 several projects in this direction have been done, like proving PSPACE completeness of a particular variant of five-in-a-row, investigating the exponential behavior of Sokoban, and implementing four-in-a-row. Where investigating complexity class is a theoretical issue, it is also of interest to investigate how instance of puzzles can be treated by computer support, in particular modern techniques like SAT/SMT solving.

Contact: Hans Zantema

Termination of many-sorted term rewriting systems (BSc/Msc)

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