Hello!

My name is Tomaz Mascarenhas. Currently I am a PhD student at Universidade Federal de Minas Gerais, working on the generation of proofs for non-linear arithmetic reasoning under the supervision of Haniel Barbosa. Previously, I was a Research Engineer for the CNRS, where I worked with multiple research projects involving OCaml, Coq, type theory and formal methods.

My main focus is to improve the usability of proof assistants. During my master's I co-developed lean-smt, a tool for integrating SMT solvers with the Lean proof assistant. Besides that, I am generally interested and always learning about functional programming, type theory, formal methods and programming language design and theory. I am also a passionate competitive programmer! Check out my Codeforces profile below.

• CF
• CV