Deivid Vale

School of Computer and Cyber Sciences

Augusta University

1120 15th Street, UH 127

Augusta, GA 30904

United States of America

I am a post doctoral researcher at the Department of Sofware Science, Radboud University, working under the NWO CHORPE project.

Recently, I was a PhD student also at Department of Sofware Science, Radboud University working under the NWO Top Project ICHOR. My PhD thesis entitled ‘‘On Semantical Methods for the Analysis of the Complexity of Higher-Order Rewriting’’ has been submitted and is currently under revision.

Research Interest

My research interests lie mainly in the intersection of Computer Science, Logic, and Mathematics. I am somewhat involved or reading a lot about the following topics:

Higher-order rewriting
Implicit complexity
Nominal Techniques
Structural Complexity
Type-2 complexity
Type-theoretical approach to complexity analysis
Foundations of functional programming
Formalization of mathematical structures (like rewriting) in Coq

Main Research Projects

At the moment, I am working on three main research topics, which I shall briefly present (in somewhat chronological order) below.

I started investigating nominal equational syntax and semantics as my master thesis research project (you can find it on the publications page). Mainly, I am concerned with reasoning about the syntax and semantics of solving negated equations inside the nominal techniques. This (ongoing) project have been producing interesting results and collaborations over the years.

My principal research inquiry, which is the main topic of my Ph.D., focuses on complexity analysis and higher-order rewriting. A term rewriting system is a model of computation where computations are modeled as a step-by-step transformation on objects. In this context, studying complexity theory basically means measuring how many steps are needed to perform some task.

More recently, I have been involved in a project to apply rewriting techniques to the field of Type-2 Structural Complexity Theory. It is very new, so more updates will follow in the coming months.

news

Jan 15, 2016	A simple inline announcement with Markdown emoji!
Nov 07, 2015	A long announcement with details
Oct 22, 2015	A simple inline announcement.

selected publications

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
conf

Nominal Equational Problems

Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho, and 1 more author

In Foundations of Software Science and Computation Structures, Mar 2021

DOI