About Me
I am a professor at EMAp/FGV (Applied Mathematics School, Getulio Vargas Foundation, Rio de Janeiro), where I have been teaching since 2010. I am also serving as Director of the CSLib Initiative (Computer Science Library in Lean) at Renaissance Philanthropy, a global open-source initiative with founding support from Amazon and Google. Through a collaboration with New York University, I contribute to DARPA's ExpMath programme, which aims to accelerate mathematics research with AI.
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 held two international research fellowships. At Microsoft Research, in 2008, I worked with the Z3 SMT Solver team (Leonardo de Moura and Nikolaj Bjørner); at SRI International, in 2009, I worked under the supervision of Natarajan Shankar.
My work in computational linguistics has produced several language resources for Portuguese processing, including contributions to the DELPH-IN consortium. 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. I have served as publication chair of the Language Resources and Evaluation Conference (LREC) and on the board of the Global Wordnet Association.
From April to December 2025, I led the Specification IDE project at Atlas Computing, part of the Formal Verification of Software initiative funded by Schmidt Sciences under their Science of Trustworthy AI programme. The project prototyped a tool to help users with no formal methods background understand formal specifications, by mapping subsections of a spec to natural language descriptions and annotating the comparison. This work contributed to a broader collaboration with CSLib and the Lean community, grounding specifications in mathematical foundations to provide strong guarantees for AI-produced software.