Massin Guerdi

I'm a PhD student in Theoretical Computer Science and Theorem Proving at LMU Munich under the supervision of Jasmin Blanchette.

My main research interests are automated and interactive theorem proving.

I currently work on slam, a λ-superposition tactic for Isabelle/HOL. See also the publication below.

I speak German and English. Feel free to address me by my first name and to use "du" instead of "Sie" in German. My pronouns are he/him.

You can send me email at <my first name>.<my last name>@ifi.lmu.de.

My office is room L 101, Oettingenstraße 67.

A Lambda-Superposition Tactic for Isabelle/HOL. Massin Guerdi. Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026. Publisher's page. Erratum: on page 120, the NegExt rule is missing a C ∨ [...] in its premise and conclusion.