I am interested in the intersection of programming languages, type systems, distributed systems and formal verification.
My PhD topic is about mailbox types, a type system for actor-style languages that reason about the content of mailboxes. This includes:
- Metatheory about programming languages and type systems
- Formalizations in proof assistants such as Rocq
- Correctness of implementations of type checkers and compilers
I am also interested in logic and all things that have to do with mechanization of concepts in proof assistants.
If you are looking for a Bachelor's / Master's thesis or guided research that fits into these topics, feel free to reach out.
Publications
Proof of Delivery: Mechanized Mailbox Types
Edgard Schiebelbein, Annette Bieniusa, and Simon Fowler
COORDINATION 2026
Models for Storage in Database Backends
Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Carla Ferreira, Gustavo Petri, and Marc Shapiro
PaPoC 2024