About Me

I am an adjunct professor at EMAp/FGV (Applied Mathematics School, Getulio Vargas Foundation, Rio de Janeiro). I am also serving as Director of CSLib (Computer Science Library in Lean) at Renaissance Philanthropy, a global open-source initiative funded by Amazon and Google. I am also a participant in DARPA's ExpMath programme on AI-assisted mathematical formalization.

My research spans formal methods, theorem proving, type theory, computational linguistics, and knowledge representation.

I finished my doctorate in Computer Science at PUC-Rio in 2010. My thesis proposed new deduction systems for description logics under the supervision of Edward Hermann Haeusler, published by Springer as A Proof Theory for Description Logics. During my Ph.D., I made two international fellowships at Microsoft Research and SRI International. At MSR, in 2008, I worked with the Z3 SMT Solver team (Leonardo de Moura and Nikolaj Bjørner). At SRI International. At SRI, in 2009, I worked under the supervision of Natarajan Shankar.

My work in computational linguistics has produced several language resources for Portuguese processing. The two main ones are the Portuguese Wordnet, available at openWordnet-PT, and Portuguese treebanks at Universal Dependencies. Other resources can be found at LR-POR and own-pt.