Deivid Vale

Institute for Computing and Information Sciences

Department of Software Science,

Radboud University

Nijmegen, NL

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

May 12, 2023	The paper “Runtime Complexity Analysis via Tuple Interpretations” has been accepted for an extended version on MSCS journal.
Apr 18, 2023	The paper “Certifying Higher-Order Polynomial Interpretations”, co-authored with Niels van der Weide and Cynthia Kop, has been accepted for presentation at ITP2023.
Apr 13, 2023	The paper “Cost–Size Semantics for Call-by-Value Higher-Order Rewriting”, co-authored with Cynthia Kop, has been accepted for presentation at FSCD2023.
Jul 15, 2022	Our paper “Runtime Complexity Analysis via Tuple Interpretations” has been accepted for presentation at LSFA2022.
Apr 19, 2021	The paper “Tuple Interpretations for Higher-Order Complexity” has been accepted for presentation at FSCD2021.

selected publications

conf

Certifying Higher-Order Polynomial Interpretations

Niels Weide, Deivid Vale, and Cynthia Kop

In 14th International Conference on Interactive Theorem Proving, 2023

arXiv DOI 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},
}

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