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 ‘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/p_droabreu0