Projects

Implicit Complexity Theory Survey

EECS 574 (Complexity Theory) survey on type theories which are sound and complete for various complexity classes.

Paper / Video

Interaction Trees & VeLLVM Tutorial

EECS 583 (Compilers) project demonstrating how to prove correctness of assembly/LLVM transformations using Interaction trees. I ran out of time to verify a full transformation but I did manage to write up a decent tutorial.

Paper /Code /Video

DARPA Programs

As a Research Scientist at Two Six Technologies, I performed on the following DARPA programs: DPRIVE, SafeDocs, V-SPELLS, HARDEN, and PEARLS.

AMS Mathematical Research Communities

Summer 2022 Applied Category Theory session. Member of Valeria de Paiva’s group investigating applications of Dialectica Categories. Partial formalization of Dialectica Categories and Dialectica Petri Nets in Agda available here.

Agda Projects

• Polynomial Functors and Dynamical Systems in Cubical Agda (code)
• MetaTheory a la Agda & Free Monads (code)