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.kappe@liacs.leidenuniv.nl.
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
