Publications
A Type-Based Approach to Divide-and-Conquer Recursion in Coq, Abreu, Pedro and Delaware, Benjamin and Hubers, Alex and Jenkins, Christa and Morris, J. Garrett and Stump, Aaron, POPL’23
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, Gallinete Team, and Cambium (Inria)
POPL’20 Poster - How Small Can We Make A Useful Type Theory?