Student Projects

(Last updated: 01/17/2023)

Looking for a student project? Did you enjoy BSc courses like Introduction to Logic, Program Correctness, and Languages and Machines? Here I collect information for BSc and MSc students at the UG interested in working under my supervision.

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

    • Specifically, 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:

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

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

  • In my research area, topics/projects can be theoretical but also practical (see below for a couple of examples).

  • Usually, I don't have a predefined list of potential research topics. In my experience, it is better 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

Strongly recommended

I highly recommend Robin Milner's Turing lecture, which provides a good overview of the motivations and intuitions underlying process calculi, and their role 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:

  • To learn about about programming calculi, both 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 the basics of session types for message-passing programs, have a look at

    • Vasconcelos: "Sessions, from Types to Programming Languages" [link]

  • For a programming-oriented introduction to session types, have a look at SePi [link], a concurrent programming language based on the pi-calculus (you can try it online)

  • 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]

  • 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 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]

  • 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.

Examples of BSc Projects

  • Bastiaan Haaksema (2021): Executable Specifications of Message-based Concurrency in Maude [link]

  • Erik Voogd (2018): Minimal Session Types [link]