teaching

I regularly teach at Ruhr University Bochum.

Functional Programming (co-taught with Clara Schneidewind)

Offered in: WS 25/26 (Moodle)

Next time to be offered: WS 26/27

This is a Bachelor-level course modeled after the course Programming I designed by Gert Smolka and taught at Saarland University since many years. The course provides a rigorous, hands-on introduction to functional programming, an influential paradigm for building reliable, maintainable, and secure software. Using OCaml, students explore key concepts such as strong static typing and advanced type systems for writing safe, composable programs. Through lectures, exercises, and case studies (including building a small programming language), they gain both practical skills and a deeper understanding of how functional languages work. The course also introduces formal reasoning about program correctness, equipping students to write functional programs and justify their reliability and security.

Foundations of Programming Languages, Verification, and Security (co-taught with Catalin Hritcu)

Offered in: SS 2025 (Moodle)

This is a Master-level course based on the books Software Foundations (by Benjamin C. Pierce) and Security Foundations (by Catalin Hritcu and Roberto Blanco). The course uses the Rocq proof assistant to introduce the formal foundations of Programming Languages, Verification, and Security. Using a proof assistant enables us to program formal proofs interactively, with proofs being machine-checked along the way. We use Rocq to define the syntax and semantics of imperative and functional programming languages, to define type systems, and to prove theorems such as type soundness. We also formalize Hoare Logic and Relational Hoare Logic in Rocq and use them to prove the correctness and security of simple imperative programs. Finally, the course introduces static and dynamic enforcement mechanisms for Secure Information Flow Control as well as their formal noninterference guarantees. We formalize Cryptographic Constant Time and Speculative Constant Time and prove in Rocq that a software defense called Speculative Load Hardening (SLH) achieves Speculative Constant Time.

Bachelor’s / Master’s Theses

I am happy to supervise Bachelor’s and Master’s theses and CS@Max-Planck research immersion labs. Please reach out if you’re interested.

Previously supervised projects:

  • Janine Lohse, Bachelor’s thesis: Model Checking for (Hyper) Temporal Stream Logic (2022)
  • Yannick Schillo, Research project: Specifying Android Apps with TSL (2020 - 2022)
  • Frederik Scheerer, Bachelor’s thesis: Monitoring Smart Contracts with RTLola (2021)
  • Julia Tillman, Bachelor’s thesis: Temporal Stream Logic for Hyperproperties (2020)
  • Matthias Cosler, Bachelor’s thesis: Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis (2019)

Before MPI-SP

Before joining MPI-SP, I served as teaching assistant and ‘‘course manager’’ at Saarland University:

Assisted Lectures During PhD:

  • Winter 2020/2021: Assistant for Basic Course Programmierung 1
    received :trophy: Busy Beaver award for outstanding teaching performance
  • Winter 2019/2020: Assistant for Core Course Verification
  • Summer 2019: Advisor for Proseminar Softwarezuverlässigkeit (Software Reliability)
  • Winter 2018/2019: Assistant for Seminar Hyperproperties

Before PhD:

  • Summer 2018: Coach for Mathematics Precourse at Saarland University
  • Summer 2017: Lecturer and Coach for Mathematics Precourse at Saarland University
    :trophy: BeStE award for student initiatives and extraordinary commitment
  • Summer 2017: Student TA for Theoretical Computer Science at the School of Informatics, University of Edinburgh
  • Winter 2016/2017: Student TA for Informatics I – Functional Programming at the School of Informatics, University of Edinburgh
  • Summer 2016: Coach for Mathematics Precourse, Saarland University
  • Summer 2016: Student TA for Concurrent Programming, Saarland University
  • Winter 2015/2016: Organizer of Didactic Seminar for Re-exam Student TAs
  • Winter 2015/2016: Supervision Student TA for Programming 1, Saarland University
  • Summer 2015: Coach for Mathematics Precourse at Saarland University, Saarland University
  • Winter 2014/2015: Organizer of Didactic Seminar for Re-exam Student TAs, Saarland University
  • Winter 2014/2015: Student TA for Programming 1, Saarland University
  • Winter 2013/2014: Re-exam Student TA for Programmierung 1, Saarland University