Research
A Type-Based Approach to Divide-and-Conquer Recursion in Coq, Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump, POPL 2023
MSc Thesis: A Translation of OCaml GADTs into Coq, Purdue University
Talks and Presentations
From Turing to Type Theory: The Rich Historical Context of Computation Invited Talk in the Summer of ‘24 at UnB, UFMG, UFPE, and FP Meeting at Gothenburg
A Translation of OCaml GADTs into Coq Master Defense in May ‘24, and Invited Talks in the Summer of ‘24 at Chalmers University, Utrecht, TU Delft, Galinette Team, and Cambium (Inria)
POPL’20 Poster - How Small Can We Make A Useful Type Theory?