Research + Projects
Contents
Research / Projects
Chamelean: Property-Based Testing for Lean via Metaprogramming
- Chamelean is an extension of Lean’s Plausible property-based testing (PBT) library, which takes user-defined inductive relations and automatically derives specialized random generators, enumerators and checkers
- I used Lean’s metaprogramming facilities to implement algorithms used by Rocq’s QuickChick PBT framework to compile inductive relations into correct-by-construction PBT generators
- Work done during an internship at Amazon Web Services, advised by Mike Hicks & Cody Roux, with collaborators at UMD (Segev Elazar Mittelman, Harry Goldstein & Leo Lampropoulos)
Mica: Automated Differential Testing for OCaml Modules
(OCaml Workshop ’24 paper) (ICFP ’23 SRC poster) (GitHub) (Web demo)
- Mica is a PPX compiler extension which automates differential testing for OCaml modules. Mica automatically generates property-testing code specialized to the interface, checking if two modules are observationally equivalent.
- Available to install via Opam
- Presented paper at the OCaml Workshop 2024 (co-located with ICFP ’24)
- Received Second Prize at the ICFP ’23 Student Research Competition
- Advised by Harry Goldstein & Benjamin Pierce
Verified Brzozowski and Antimirov Derivatives
- Mechanized Coq proofs about the equivalence of Brzozowski derivatives, Antimirov derivatives, and their zipper representation (Edelmann 2020)
- Implemented executable derivative-based regex matchers in OCaml, tested using QuickCheck
- Joint work with Laura Zielinski, advised by Jules Jacobs and Nate Foster
- Final project for CS 6115 (Certified Software Systems)
Flattening the Bril Intermediate Representation
- More details in the blog post about this project!
- Used Rust to implement a flattened representation for the Bril IR & an interpreter that works natively over the flattened representation
- Joint work with Sam Breckenridge and Katherine Wu, advised by Adrian Sampson
- Final project for CS 6120 (Advanced Compilers)
Mechanized Type Soundness Proofs for the Hindley-Milner Type System
- Mechanized type soundness proofs for the Hindley-Milner (or “Damas-Milner”) type system using the locally nameless representation in Coq, along with the LNgen & Ott metatheory tools.
- The proofs are for the non-syntax-directed version of the HM type system, as presented in Peyton Jones et al. (2007).
- Joint work with Gary Chen & Zed Wu, advised by Stephanie Weirich
- Final project for CIS 6700 (Advanced Topics in Programming Languages)
Lectures
seL4 : Formal Verification of an OS Kernel (Paper Presentation)
- Slides for a paper presentation I gave for CS 6410 (Advanced Systems)
- In these slides, I present Klein et al’s (SOSP 2009) paper on the seL4 operating system and its role in the history of formally-verified OSes
Programming in the Untyped λ-calculus
- Slides for a talk I gave for CIS 6700 (Advanced Topics in Programming Languages)
-
In these slides, I cover the Church & Scott encodings of various
datatypes in the untyped λ-calculus,
following the presentation in Pierce’s Types & Programming Languages textbook.
Parsers in Haskell
- Slides for a guest lecture for CIS 1940 (Introduction to Haskell)
-
In these slides, I cover monadic parser combinators (à la Parsec),
Haskell’s
Applicativetypeclass & testing parsers using QuickCheck. -
I also designed an assignment
where students build a parser for Lisp-style S-expressions using
Applicativefunctors, and test the correctness of their parser using round-trip properties in QuickCheck.
Other Programming Projects
SQL to Pandas Translator
- A tool for translating SQL queries into equivalent Pandas queries, implemented in Haskell.
- I worked on implementing a parser for SQL queries using monadic parser combinators, and verifying the correctness of the parser using QuickCheck.
- Joint work with Jason Hom, mentored by Joe Cutler
- Final project for CIS 5520 (Advanced Programming)
PennOS
- A Unix-esque operating system implemented in C (~10k lines of code)
- I worked on the OS kernel, in particular implementing the scheduler and handling signals/process statuses, as well as integrating the kernel with the shell.
- Joint work with Mati Davis, John Smith, Rohan Verma, Keshav Ramji
- Final project for CIS 5480 (Operating Systems)