PhD position in Programming Languages and Logic, Leiden University (The Netherlands)

We invite applications to a fully funded 4-year PhD position at the intersection between logic and programming languages, on the topic "Expressivity of Imperative Programs", to be hosted at Leiden University. The application deadline is June 30, 2025.

The semantics of programming languages are often modeled as abstract machines that evolve through interaction with their environment, raising the question of whether every machine behavior can be captured by a program in a given language. This question has practical implications, such as in compiler optimizations and decompilation for tasks like malware analysis. However, theoretical limits exist: languages lacking non-local control flow constructs like goto or break cannot express all machine behaviors. This issue, rooted in debates dating back to the 1980s, continues to inspire research, especially into the expressiveness of structurally constrained control flows. This PhD project explores these questions through the lenses of programming languages, automata theory, and process algebra.