Student Projects
(Last updated: 27/09/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 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 linear types for the pi-calculus, 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]
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 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.