Rishikesh Vaishnav (Rish)

I am a PhD student (started in March 2023) in Deducteam supervised by Frédéric Blanqui. My PhD project is the design and implementation of a tool to translate Lean to and from Dedukti.

Contact

You can reach me at: rishikesh-hirendu.vaishnav (at) inria (dot) fr.

Research Interests

• proof systems interoperability -- translation of mathematical libraries and programs between proof assistants, common tools for user interfaces and program extraction etc.
• interfaces and ergonomics of proof assistants
• proof assistants as programming languages, program verification
• Automation/machine learning applications to code generation/verification and general theorem proving

Publications

Rishikesh Vaishnav. Formalizing the Beginnings of Bayesian Probability Theory in the Lean Theorem Prover. Master's Thesis, UC San Diego, 2022. eScholarship.

Rishikesh Vaishnav. A Term-Patching Framework for Eliminating Definitional Equalities in Lean (Work-in-Progress). 2024. ffhal-04813916f. HAL