Deivid do Vale

I am an assistant professor (tenure track) in Theoretical Computer Science at the Department of Mathematics at the University of Brasilia. Prior to that, I was a post-doctoral researcher in the Department of Computer Science at the School of Computer and Cyber Sciences, Augusta University — United States. I work with Clément Aubert in the NSF-funded project Concurrency In Reversible Computations.

I also worked as a post-doctoral researcher at the Department of Sofware Science, Radboud University, working with Cynthia Kop in the CHORPE NWO project.

My PhD thesis entitled ‘‘On Semantical Methods for Higher-Order Complexity Analysis’’ can be found at https://repository.ubn.ru.nl/handle/2066/304473.

Research

My research interests lie broadly on the intersection of Theoretical Computer Science, Formal Verification, and Automated Reasoning. More specifically, I am currently investigating how we can combine notions of reversible computability and the λ-calculus. This ought to lead us to an interesting λ-calculae that we can use — for instance — for reasoning about program semantics, implicit computational complexity, and higher-order functional programming. There will be a formalization of these results, which I plan to make publicly available in the near future. For more information on this project and the activities of our group, please check https://github.com/CinRC.

In addition, I am somewhat involved in research projects or reading a lot about the following topics:

• Higher-Order Rewriting
  • complexity analysis
  • interpretation methods
  • termination
• Implicit Complexity
  • type-2 complexity
  • type-theoretical approaches to implicit complexity analysis
• Nominal Techniques
  • nominal syntax
  • nominal unification/disunification
• Formalization of mathematical structures (like rewriting) in Rocq
  • check for instance the nice Nijn/Onjin project, developed in collaboration with Niels van der Weide and Cynthia Kop