I am currently a PhD student at Purdue University. I work with Programming Languages, Proofs and Theorem Provers. More specifically on Coquedille, a compiler from the intrinsic type theory of Coq to the extrinsic type theory of Cedille.
Host of the Type Theory Forall Podcast
My advisor is Prof. Benjamin Delaware.
The summer of ‘19 I have been an intern at Galois Inc.
I got my BS in Computer Science at the University of Brasilia, under Rodrigo Bonifacio in 2017.