Deivid Vale

Department of Computer Science

Augusta University

Augusta, GA

United States

I am 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.

Recently, I 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

news

Aug 06, 2025	Journal paper accepted at the Logical Methods in Computer Science
Feb 01, 2025	Starting a Postdoctoral Research Fellow Position at Augusta University

selected publications

conf

On Basic Feasible Functionals and the Interpretation Method

Patrick Baillot, Ugo Dal Lago, Cynthia Kop, and 1 more author

In Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, 2024

DOI

conf

Certifying Higher-Order Polynomial Interpretations

Niels Weide, Deivid Vale, and Cynthia Kop

In 14th International Conference on Interactive Theorem Proving, 2023

DOI arXiv Bib Code

@inproceedings{weide:vale:kop:23,
  author = {van der Weide, Niels and Vale, Deivid and Kop, Cynthia},
  title = {{Certifying Higher-Order Polynomial Interpretations}},
  booktitle = {14th International Conference on Interactive Theorem Proving},
  pages = {30:1--30:20},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  year = {2023},
  volume = {268},
  editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2023/18405},
  urn = {urn:nbn:de:0030-drops-184051},
  doi = {10.4230/LIPIcs.ITP.2023.30},
  annote = {Keywords: higher-order rewriting, Coq, termination, formalization},
  selected = true,
  bibtex_show = true
}

conf

Cost-Size Semantics for Call-By-Value Higher-Order Rewriting

Cynthia Kop, and Deivid Vale

In 8th International Conference on Formal Structures for Computation and Deduction (FSCD), 2023

DOI