Working with Kleene Algebras and related automated tools and methods

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. See also general concerns.

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 system/programs can be written using the synchronous and concurrent variants of Kleene algebra. This topic would involve working with examples.

See project link. for programming.


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.

See project link. on modelling.

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.

See project link. on automated theorem provers.

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.

See project link.

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.

See project link.



Tags: modelling, Kleene algebra, concurrency, Dynamic logic, concurrent programming, reasoning, Key tool, automated theorem provers, programming languages, algebraic specification, object-orientation
Published Aug. 25, 2017 9:37 AM - Last modified Oct. 25, 2019 12:15 PM


Scope (credits)