Courses

I currently coordinate and teach the following courses in the Bachelor Computing Science and the Master Computing Science.

Course  
Languages and Machines (BSc, 2B) Schedules
Models and Semantics of Computation (MSc, 1A) Schedules
Basic Approaches to the Semantics of Computation (BSc, 1B) Schedules

Supervised Projects (BSc and MSc)

General Information (Last updated: March 21, 2026)

Looking for a student project? Did you enjoy BSc courses like Languages and Machines and Basic Approaches to the Semantics of Computation? Here I collect information for BSc and MSc students interested in working under my supervision.

  • Broadly speaking, I look forward to supervising projects on methods and tools for program verification.

    • I am interested in rigorous programming models for message-passing concurrency, in particular process calculi.

    • On top of process calculi, I investigate verification techniques based on type systems, in particular session types.

  • In addition to projects on process calculi + session types, I also enjoy supervising projects on:

    • Logical foundations of concurrency. This concerns formal connections between session types and linear logic.

    • Concurrency and formal models of computing. One current interest concerns models for reversible computation, and how such models can help to debug concurrent programs.

  • In my research area, topics/projects can be theoretical but also practical.

  • Rather than having a predefined list of research topics, I prefer to sit together and design a research topic of mutual interest, tailored to your interests and ambitions.

  • Coming up with a good research topic requires some independent study on your side; see pointers to resources below.

Suggested Resources

I highly recommend Robin Milner’s Turing lecture, which nicely overviews of the role of process calculi as foundational models of concurrency and interaction:

  • Milner: “Elements of Interaction” [link]

Further pointers

In addition to “Elements of Interaction”, you may find the following pointers useful:

  • If you are not yet familiar with research papers in Computer Science, you may start from the following short read:
    • Keshav: “How to Read a Paper” [link]
  • For a general introduction to programming language semantics, you can read the following tutorial:
    • Hutton: “Programming Language Semantics - It’s Easy As 1,2,3” [link]
  • To learn about about programming calculi, sequential and concurrent, you can start by reading
    • Pierce: “Foundational Calculi for Programming Languages” [link]
  • To learn about the pi-calculus, the paradigmatic calculus of concurrency, you can start with the first two sections of
    • Parrow: “An Introduction to the pi-calculus” [link]
  • To learn about linear logic, the logic of consumable (computational) resources, you can read the following tutorial
    • Wadler: “A Taste of Linear Logic” [link]
  • To learn about the pi-calculus equipped with linear types (i.e., types based on linear logic), you can read
    • Kobayashi, Pierce, and Turner: “Linearity and the pi-calculus” [link]
  • To learn the basics of session types for message-passing programs, have a look at
    • Vasconcelos: “Sessions, from Types to Programming Languages” [link]
  • To learn about the Curry-Howard correspondence (aka propositions as types) you can read
    • Wadler: “Propositions as Types” [link]
  • To learn about the Curry-Howard correspondence for concurrency (aka propositions as sessions) you can read
    • Caires, Pfenning, and Toninho: “Towards Concurrent Type Theory” [link]
  • To learn about multiparty session types, which have multiple practical applications, you can read
    • Yoshida and Gheri: “A Very Gentle Introduction to Multiparty Session Types” [link]
  • A starting point for learning about reversibility in concurrency is the following paper
    • Lanese, Mezzina, and Tiezzi: “Causal-Consistent Reversibility’ [link]

Contact me!

Once you have read one or several of the papers above, feel free to send me an email to schedule a meeting.