Student Projects

(Last updated: 01/17/2022)

Looking for a student project? Here I collect information for BSc and MSc students at the UG interested in working under my supervision.

• Broadly speaking, I supervise 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 often supervise 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 this space, research topics can be theoretical but also practical (see below for examples).

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