PhD in Logic (Proof Theory) – 2011 ~ 2014
Vienna University of Technology – Vienna, Austria
Cut-elimination by resolution in intuitionistic logic (thesis)
Adviser: Alexander Leitsch

MSc in Logic (Proof Theory) – 2009 ~ 2010
Federal University of Minas Gerais (UFMG) – Belo Horizonte, Brazil
Specification of systems using linear logic with subexponentials (in Portuguese)
Adviser: Elaine Pimentel

BSc in Computer Science – 2004 ~ 2008
Federal University of Minas Gerais (UFMG) – Belo Horizonte, Brazil

The underlying common theme of my research is the use of formal methods, more specifically proof theory, for reasoning about systems. I am particularly interested in reasoning which can be automated. As a result, my research involves logic, proof systems, logical frameworks, proof search, proof assistants, and theorem provers.

Here are a few topics I work on:

• Linear logic
  Linear logic is a resource conscious logic where propositions can be "consumed" (i.e., they are not always true). This makes it suitable for encoding a variety of stateful systems. I have developed a logical framework based on (an extension of) linear logic, called SELLF, which can be used to reason about sequent calculus systems.
   
• Cut-elimination via resolution
  In proof theory, proofs can be represented as trees using sequent calculi, and the use of lemmas are "special nodes" (called cuts) in these trees. Lemmas can be systematically eliminated using a method developed by Gentzen in 1934. During my PhD I have worked on a different method for eliminating lemmas with the help of theorem provers.
   
• Formalizations
  Some results in proof theory (identity expansion, cut-elimination, etc.) require the check of many similar cases of a combinatorial nature. I have been involved in the formalization of such results in interactive theorem provers. Mechanically checking these proofs increases their reliability since humans usually do not have the patience to check every case and are prone to errors.
   
• CLF
  The concurrent logical framework CLF was developed at CMU for encoding concurrent systems. It is a type-theoretical framework based on linear logic. I am part of the research project for developing a reasoning engine to prove properties about specifications in CLF.
   
• General proof theory
  Proof theory and proof systems are the tools I use for formalizations, but I am also interested in them as standalone objects. I have been involved in the development of the Encyclopedia of Proof Systems, a community effort to document proof systems in a concise and didactic manner. I have also briefly worked on the complexity of proofs in different systems, proof translations, and introduction of lemmas (cuts).

Proof theory, linear logic, logical frameworks, theorem proving, formal reasoning

See DBLP.

• 15-110 Principles of Computing
• 15-150 Principles of Functional Programming 
• 15-295 Competition Programming and Problem Solving
• 15-312 Foundations of Programming Languages 
• 15-316 Software Foundations of Security & Privacy
• 15-317 Constructive Logic