About me
Before joining UMich, I completed my PhD in the Computer Science Department at Carnegie Mellon University. I worked with Limin Jia and Farzaneh Derakhshan on guaranteeing the correctness of programs that run intermittently.
Before that, I worked with Jan Hoffmann on quantitative analysis through the CMU REUSE program. We worked on formulating polymorphism for Resource Aware ML, a language capable of inferring tight resource bounds for OCaml programs. This was my introduction to programming languages research.
And before all that, I completed my undergraduate at the University of Kansas where I double-majored in computer science and mathematics, and minored in visual arts (emphasis in painting). While there, I was a research assistant under the guidance of Dr. Suzanne Shontz in scientific computing. I worked on developing quality metrics for high-order meshes for modeling the human heart.
Outside of research, I enjoy oil painting π¨, running ππ»ββοΈ, cooking π₯, gardening πͺ΄, exploring πΊοΈ, and cat parenting π±.
What i'm working on
-
Glacier
The first provably correct supports for concurrent intermittent programs, including a co-designed runtime and type system.
-
Modal Crash Types
Crash Types that characterize the logical underpinning of intermittent computing in terms of its key operations -- crash, restore, and commit -- via adjoint logic.
-
Usage-Aware proof calculus for dL
A refinement of dL that statically detects modeling errors in formulae by inspecting their proofs.