I am a PhD student at IT University of Copenhagen under supervision of Marco Carbone and Jesper Bengtson. I am part of their Program, Logics and Semantics group (PLS). I am interested in program verification through the use of proof assistants, as well as techniques in general for the analysis and verification of programming languages. I am currently working on a mechanisation of multi party session types, as they were initially formulated [1].

Publications

• A sound and Complete Projection for Global Types (ITP23) link

Mechanisation projects

• MSc thesis: A Propositional Calculus for Contract Specification (Coq) pdf
• Verified Rewriting of MFOTL Formulas (Isabelle) pdf
• Soundness and Completeness of Verification Conditions wrt to Hoare Logic (Twelf)

[1]: Multiparty Asynchronous Session Types: Kohei Honda, Nobuko Yoshida, Marco Carbone