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.

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.