Nipun  Pitimanaaree

Nipun Pitimanaaree

Scholar Title

MIT EECS | Hewlett Foundation Undergraduate Research and Innovation Scholar

Research Title

NVL Coq Spark SQL Formalization and Optimization





Research Areas
  • Software Design and Programming Languages

Adam Chlipala


This project focuses on verifying correctness of Spark’s SQL operations and optimizations via Coq, a formal proof-management system. The first part of this project was done in my previous UROP experiences, which involved formalizing translation of SQL operations to builders, a core feature behind Spark for back-end optimization. After successfully developing the basic formalization, the goal of this SuperUROP project is to prove some optimizations for the formalized Spark’s SQL operations so that we can translate SQL queries to our formalized and optimized builders for fast querying while preserving the correctness of the output.


I’m participating in SuperUROP because I want to research and explore program verification that is, how to ensure that a program is semantically correct and runs as intended. I also want to learn more about tools and techniques for formalizing correctness of a program.

Back to Scholars