I'm a Postdoc working in the Computational Logic Center under Dr. J. Garrett Morris. My primary focus is PL theory and mechanization using tools like Agda and Lean4. I also work on the formal theory and implementation of Cedille2.