Publications

• Structural temporal logic for mechanized program verification [arxiv] [code] (in submission).
• Choice Trees: Representing and reasoning about nondeterministic, recursive, and impure Programs in Coq [eprint][code], Journal of Functional Programming, Special POPL 2025 edition (in submission).
• Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization [extended] [code], Proceedings of the ACM on Programming Languages, OOPSLA, 2024, Pasadena, CA, 2024.
• Reef: Fast Succinct Non-Interactive Zero-Knowledge Regex Proofs [eprint] [code], USENIX Security, Philadelphia, PA, 2024.
• Efficient Representation of Numerical Optimization Problems for SNARKs   [eprint] [code], USENIX Security, Boston, MA, 2022.
• Normalization-by-evaluation and Metaprogramming with PHOAS   [paper] [video], POPL SRC, 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], NASA Formal Methods (NFM), April 2019, Houston, TX.
• Parallel Back-End for the Halide Image Processing Language   [paper] [poster], MIT Undergraduate Research Journal 2015, SuperUROP with Saman Amarasinghe, Cambridge, MA.

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 issuer and number UFID18-1000.