Hello! I’m Rish, a PhD student in computer science at the Laboratoire Méthodes Formelles (LMF) in ENS Paris-Saclay, part of the Deducteam research group. I am supervised by Frédéric Blanqui on the design and implementation of a tool for translating between Lean and Dedukti, and I expect to complete my doctoral studies in March 2026.

I’m generally interested in the use of proof assistants for mathematical formalization and synthesis, with my doctoral research focusing on the topic of proof translation for improved interoperability between proof assistants based on different foundations.

My broader research interests are around the topic of using proof assistants such as Lean as platforms for the synthesis of verified structural artifacts starting from domain-specific, user-provided symbolic specifications, background theories and related proof automation, primarily through the design of proof-guided search spaces for synthesis. At the moment, I am particularly thinking about possible applications of synthesis techniques in the areas of program synthesis and symbolic task planning for humans and autonomous robots.

I am currently actively on the search for post-doctoral/full-time research positions! Please feel free to contact me at the email above for any related inquiries.

Publications

PhD thesis

Conference papers

Workshop papers

Master’s thesis

Talks

Education

• B.S. Computer Science, UC San Diego, 2019
• M.S. Computer Science, UC San Diego, 2022
• (current) PhD Computer Science, ENS Paris-Saclay, projected completion in March 2026

Community service

• Artifact Evaluation Committee, ICFP 2025.