Publications

• Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report) [paper] [artifact], Proceedings of the ACM International Conference on Functional Programming (ICFP), Indianapolis, IN, 2026.
• Lazy Validation and Self-Healing for Agentic Programs [paper][code], Proceedings of the ACM Workshop on Principles of Agentic Engineering (PAgE), Programming Language Design and Implementation (PLDI), Boulder, CO, 2026.
• Correct Programs, Executed Correctly: Verifying Specifications and Executions [thesis] (Doctoral Thesis, University of Pennsylvania, 2025).
• Structural temporal logic for mechanized program verification [arxiv] [code], Proceedings of the ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Singapore, 2025.
• Choice Trees: Representing and reasoning about nondeterministic, recursive, and impure Programs in Coq [eprint][code], Journal of Functional Programming (JFP), Special POPL 2025 Edition.
• Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization [extended] [code], Proceedings of the ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pasadena, CA, 2024.
• Reef: Fast Succinct Non-Interactive Zero-Knowledge Regex Proofs [eprint] [code], Proceedings of the USENIX Security Symposium (USENIX Security), Philadelphia, PA, 2024.
• Efficient Representation of Numerical Optimization Problems for SNARKs [eprint] [code], Proceedings of the USENIX Security Symposium (USENIX Security), Boston, MA, 2022.
• Normalization-by-evaluation and Metaprogramming with PHOAS [paper] [video], Proceedings of the ACM Student Research Competition (SRC), Principles of Programming Languages (POPL), Philadelphia, PA, 2022.
• Extracting and optimizing low-level bytecode from high-level verified Coq   [paper] [code], Master’s Thesis, PDOS at CSAIL, MIT.
• MCQC: Extracting and optimizing formally verified code for systems programming [paper] [code] [slides], Proceedings of the International Symposium on NASA Formal Methods (NFM), Houston, TX, 2019.
• Parallel Back-End for the Halide Image Processing Language [paper] [poster], MIT Undergraduate Research Journal, SuperUROP with Saman Amarasinghe, Cambridge, MA, 2015.

Tech Conference Talks

• Sharing is caring; Centralized PKI and masking for multi-organization blockchain sharing [paper], Proposal, UC Berkley blockchain group, San Francisco, CA, 2017.
• Data-aware NGINX for Distributed Machine Learning [talk] [code], Nginxconf 2017 Annual Nginx Developer Conference, September 2017, Portland, OR.
• Auto-scalable microservices for Machine Learning [talk] [client] [server], Dockercon 2017 Annual Docker User Conference, April 2017, Austin, TX.
• Secure and energy-efficient sampling of mobile sensors on iOS and Android [conference], MadCon 2017 Annual Mobile development student conference, June 2017, Austin, TX.

Term papers

• Evaluating correlation between saliency maps and the solution of maze puzzles   [paper] [notebook], Final paper for 6.861J Computational Theory of Intelligence, Spring 2019, CSAIL and Brain and CogSci, MIT, Cambridge, MA.
• PAL: Progressive Authentication for Linux System   [writeup] [code], Final project for 6.858 Computer Systems Security 2013, PDOS CSAIL, Cambridge, MA.
• A collaborative text editor   [paper], Final paper for 6.033 Computer Systems Engineering, won Excellent Writting Sample award, 2012, PDOS CSAIL, Cambridge, MA.

Patents

• Privacy preserving System for Machine-Learning Training Data, Filed Mar 2, 2018 Patent numbers US-10601786-B2, US-20180255023-A1.
• Authorization Policy Validation, Filed Nov 28, 2022 Patent number US-12261888-B2.