This is a general topic regarding the foundations of programming languages and their semantics. Here the student can choose various topics to focus on, depending on the interest, which we find out together through discussions.
One can do various kinds of MSc theses, starting from just programming a simple tool related to some variant of Keene algebra, or a literature study, or doing modelling of real systems, or using existing tools for Kleene algebras like proof assistants, or doing mathematical proofs.
Ask for discussions with one of the supervisors, for more information or variations of the project.
| supervisors | Christian Johansen |
| Olaf Owe | |
| Martin Steffen | |
| Uli Fahrenberg | |
| Georg Struth |
Programming with or for Kleene Algebras
This topic involves working with programming languages constructs, at a basic level. It is known that Kleene algebra with tests (see the work of Dexter Kozen and the KAT prover) is at the basis of essential programming constructs. This topic would investigate what kind of systems and programs can be written using the synchronous and concurrent variants of Kleene algebra. This topic would involve working with examples.
Modelling
This topic would involve modeling examples of systems using Kleene algebra (for sequential/regular systems) and Synchronous or Concurrent Kleene algebra (for systems involving notions of concurrency). This topic may also involve working with other associated formalisms and languages for modeling systems; formalisms which have close connections with Kleene algebra, like translations and correlations. For the more new concurrent/synchronous variants of Kleene algebra one may build formalisms/languages/tools on top of the algebraic language, and use those for modeling.
Formal tools for Kleene Algebras
This projects involve the use of theorem provers like the general Isabelle or Coq, or specialized provers for equational systems like Prover9. One would have to start from existing work on Kleene algebra and related theorem provers, and work its way to the new formalism of Synchronous Kleene Algebra (or the related Concurrent Kleene Algebra). This project can involve either just using existing tools and checking various useful theorems, or may involve building extensions and libraries specific for these two concurrent variants of Kleene algebra.
Reason about programs with Dynamic algebras and work with the Key tool
This project involves understanding Dynamic Logic (see the book of David Harel, Dexter Kozen and Jerzy Tiuryn; available also at the IFI library). This powerful method of checking functional/logical properties of programs was implemented in the tool Key. The master project would involve surveying literature and working on concrete case studies.
Algebraic Theory of Object Oriented Programming
This topic involves the investigation of algebraic theories of programming, and then reach the recent few works on algebraic approaches to object-oriented concepts of programming. Depending on the maturity of the student, this topic would end with touching on one of the many open research questions. We may also work with concurrent OO languages.