During his PhD studies, Sergei Stepanenko investigated semantics of programming languages. Computer programs have been ubiquitous for decades, and so have the bugs and errors that come with them. Over time, programming becomes ever more embedded in critical systems, the consequences of these errors can be severe. To prevent them, we need rigorous methods to reason about program semantics. However, modern languages often exhibit features with intricate behavior.

Sergei explored semantics of features found in programming languages. His work focuses on three main contributions:

• Developing a mathematical model for a language featuring Generalized Algebraic Datatypes, a key construct in languages such as Haskell and Ocaml.
• Extending the theory of Guarded Interaction Trees to support context-dependent effects, and demonstrating applications to features like call-with-current-continuation (call/cc) and delimited continuations.
• Simplifying the construction of solutions to recursive domain equations and implementing the approach in the Rocq Prover, making it easier to mechanize semantic models.

Together, these contributions advance our ability to reason about complex program behavior with mathematical precision.

The PhD study was completed at Department of Computer Science, Faculty of Natural Sciences, Aarhus University.

This summary was prepared by the PhD student.

Time: Thursday, 6 November at 13:00
Place: Building 5342, room 333, Department of Computer Science, Aarhus University, Åbogade 34, 8200 Aarhus N.
Title of PhD thesis: Formal Reasoning for Modern Programming Languages
Contact information: Sergei Stepanenko, e-mail: sergei.stepanenko@cs.au.dk, tel.: +45 28732235
Members of the assessment committee:
Professor Rasmus Ejlers Møgelberg, Section for Theoretical Computer Science, IT University of Copenhagen, Denmark
Inria researcher (chargé de recherche) Yannick Zakowski, Inria Paris, Cambium research group, France
Associate Professor Hans-Jörg Schulz (chair), Department of Computer Science, Aarhus University, Denmark
Main supervisor: Professor Lars Birkedal, Department of Computer Science, Aarhus University, Denmark
Language: The PhD dissertation will be defended in English

The defence is public.
The PhD thesis is available for reading at the Graduate School of Natural Sciences/GSNS, Ny Munkegade 120, building 1521, 8000 Aarhus C