I am Associate Professor of Computer Science at Instituto de Computação (Computing Institute) of Universidade Federal Fluminense (UFF), I lead the Theoretical Computer Science Research Group at the Computing Institute of UFF and I am a member of FADoSS research group at Universidad Complutense de Madrid. I am also a collaborator of TecMF at PUC-Rio and TCS Co-Innovation Network partner. I have obtained my PhD. from Pontifícia Universidade Católica do Rio de Janeiro in 2001. During my PhD., I have been a visiting scholar at the Computer Science Laboratory of SRI International. I was a postdoc researcher at the Computer Science Department of the University of Illinois at Urbana-Champaign, Computer Science Department of Swansea University, Facultad de Informática de la Universidad Complutense de Madrid and Informatics Department of Pontifícia Universidade Católica do Rio de Janeiro. My main research interests are formal methods and semantics of programming languages. A large part of my research has Rewriting Logic as its underlying logical and semantic framework with the Maude system. The Maude MSOS Tool (MMT), developed together with Fabricio Chalub, is a good example, and so are BMaude and the Π Framework. Recent work was also devoted to applied research with Description Logics, using OWL API, Hermit Reasoner and DL Learner library. The ECore Consistency Checker (ECC), developed together with Cássio Santos, is a representative of this research. My current research interests include Intuitionistic Type Theory and Formal Compiler Construction. The Lean Prover, developed mainly by Leonardo Moura at Microsoft Research, provides (brilliant) tool support for this research.