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.

My advisor is Prof. Benjamin Delaware.

The summer of ‘20 I was an intern at Nomadic Labs, translating Gadts from OCaml to coq for coq-of-ocaml.

The summer of ‘19 I have been an intern at Galois Inc.

Before starting my PhD in ‘18 I was an intern at Sifive under Murali Vijayaraghavan. Worked on the formalization of the floating point unit using Coq and Kami.

I got my BS in Computer Science at the University of Brasilia, under Rodrigo Bonifacio in 2017.


Pedro da Costa Abreu Júnior
Email: (\ x -> x@purdue.edu) pdacost
Github: https://github.com/pedrotst
Instagram https://www.instagram.com/p_droabreu/
Twitter https://twitter.com/etapedro