Hello! I'm a doctoral student at EPFL working in the Laboratory for Automated Reasoning and Analysis (LARA) with Prof. Viktor Kunčak , interested in program verification, theorem proving, and proofs in general. Mostly fueled by mortal fear of a machine takeover.
See also: my EPFL directory page.
My current research revolves around the use of Constrained Horn Clauses (CHCs) as a basis for expressing and exchanging problems about programs. I am interested in increasing expressiveness of and trust in current CHC-based program verifiers by modularizing their certificates and checking them with interactive and automated theorem provers.
I am involved in the development of the Stainless program verifier focusing primarily on its backend, Inox, and of the Lisa proof assistant for first-order logic.
You can find my list of publications on Google Scholar.During my undergraduate studies, my work revolved around robust temporal logics, their mathematical structure, and approaches to utilizing them in data mining, pattern detection, and causal inference. My advisors were Prof. Krishna S and Prof. Ashutosh Gupta.
Alongside my work in logic, my Bachelor's Thesis was focused on information-theoretic error bounds for quantum machine learning systems (formally, VQAs), with Prof. Sai Vinjanampathy as my advisor. A copy can be found here.
I like to learn about and collect stupid and often archaic things in my free time. Talk to me about headphones, keyboards, typewriters, or fountain pens.
When I'm not making impulse purchases, I'm probably cooking.
email: sankalp.gambhir@epfl.ch sankalp.gambhir42@gmail.com
office: BC 355, EPFL
github: sankalpgambhir