I am currently a PhD student at Purdue University. I work with Programming Languages,
Proofs and Theorem Provers. More specifically on
compiler from the intrinsic type theory of Coq to the extrinsic type theory of
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
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 -> firstname.lastname@example.org) pdacost