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". The application deadline is June 30, 2025.
Project description: 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. Responsibilities: The candidate will be embedded in the Theory cluster at the Leiden Institute of Advanced Computer Science (LIACS), supervised by Dr. Tobias Kappè and Prof. Dr. Marcello Bonsangue from the System Modelling and Analysis lab. More information about the lab can be found at https://www.universiteitleiden.nl/en/science/computer-science/research/theory. The successful candidate will conduct original and novel research at the intersection of programming language semantics, automata theory, and algebraic reasoning, publish and present scientific articles in top theory venues, contribute to educational activities as a (head) teaching assistant and finally write a PhD thesis detailing the outcome of the research activities. Selection criteria: * A master's (or equivalent) degree in Computer Science, Mathematics, Logic, or a highly related field; * Affinity with formal methods, including an understanding of basic of automata theory, formal languages, algorithms, and computability --- i.e., foundational computer science theory. Candidates with a background in mathematics or logic should be able to pick up on these topics relatively quickly; * Intrinsic motivation to perform foundational computer science research, internalize with cutting-edge theory, and synthesize new results; * Prior experience with academic writing (existing published work is not strictly necessary, but would help strengthen an application); * Openness to picking up new skills, such as how to use proof assistants like Rocq, Lean or Isabelle (prior knowledge of these is not required); * Excellent proficiency in English, both spoken and written (Dutch is not required, but LIACS does subsidize optional Dutch language courses); * Willingness to participate in educational activities; * Good research, writing, presentation, and teamwork skills. More information, including instructions on how to apply, can be found at https://www.universiteitleiden.nl/en/vacancies/2025/q2/15703-phd-candidate-on-expressivity-of-imperative-programs. For inquiries, contact Tobias Kappé at t.w.j.ka...@liacs.leidenuniv.nl. -- [LOGIC] mailing list, provided by DLMPST More information (including information about subscription management) can be found here: http://dlmpst.org/pages/logic-list.php
