Aalok Thakkar: Research

N.S. Bendre, Cosmos in the Making (1963)
N.S. Bendre, Cosmos in the Making (1963)

My research focuses on logic in computer scienceThe study of formal systems for reasoning about truth, inference, and computation. and its applications to programming languagesThe design, semantics, and implementation of languages used to express computational processes. and automata theoryThe study of abstract models of computation and formal languages.. I also work on pedagogy and on interdisciplinary questions in computational sustainabilityThe application of computational methods to problems in environmental and social sustainability..

Formal Methods and Logic

The following three tracks are active areas of research:

  1. Program synthesis. How do we construct a program from a specification? My doctoral work synthesised relational queries from input-output examples (PLDI 2021, VLDB 2023, OOPSLA 2023). I now study what to synthesise when the specifications cannot all be met: a program that satisfies a maximal subset of them. This survey is a good introduction to the area.
  2. Reliability estimation. Given a program and its operational input distribution, how often does a condition of interest hold? We combine symbolic and statistical methods to answer this with a certified error bound (ATVA 2026, Distinguished Paper, with Arnab Ray).
  3. DiagonaLean. With TVH Prathamesh and Akhilesh Balaji, we are building frameworks and tactics for formalising undecidability results in Lean 4 (RHPL 2026).

In general, I am interested in programming languages, logic, and formal methods.

These projects are supported by ANRF through the Prime Minister Early Career Research Grant, and by an Ashoka VSAC Young Faculty Grant.

Pedagogy

I design curricula and tools for teaching computer science when AI tools can write most introductory code:

  1. Correctness first. Students write specifications and proofs alongside code, so that working code is not taken as a proxy for understanding (BOOP, COMPUTE 2025; ITiCSE 2026).
  2. Socratic tutors. LLM tutors that withhold direct solutions and track student misconceptions across a dialogue (COMPUTE 2025; ITiCSE 2026).
  3. Accessibility. Making computer science courses accessible to students with visual impairments (COMPUTE 2025).
  4. Circle of Joy. Using AI to assist English language learning, with Devapriya Roy and Annie Baxi, supported by an Ashoka VSAC Transdisciplinary Research Grant.
  5. Ancient algorithms. Teaching algorithms in their historical and cultural context, with attention to classical Indian contributions (COMPUTE 2025).

Apart from Circle of Joy, these projects are supported by the Mphasis Foundation through the Mphasis AI & Applied Tech Lab at Ashoka.

Computational Sustainability

I work on projects that bring together computation and the environment:

  1. Darjeeling Revival Project. We develop statistical models to estimate carbon captured by enhanced rock weathering in northern Bengal, supported by Alt Carbon through the Darjeeling Revival Fellowship.
  2. Animal acoustics. With Meghna Agarwala and Nandini Chatterjee Singh, we detect elephant vocalisations in field recordings, supported by an Ashoka VSAC Transdisciplinary Research Grant.
  3. OpenGIS India. With Meghna Agarwala, we use GIS and remote sensing to study forest dynamics, land use, forest fires, floods and river dynamics, and human-animal conflict across India.