Talks

• Sulfur: substitution generation in Rocq using a logical framework. (2025, slides)
  This work was done during an internship with Théo Winterhalter.

• Code generation via meta-programming in dependently typed proof assistants. (2025, slides)
  This work was done during an internship with Yannick Forster.