Deivid Vale

(λxyz. xyz) deividvale (at)


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.


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

  1. Certifying Higher-Order Polynomial Interpretations
    Niels Weide, Deivid Vale, and Cynthia Kop
    In 14th International Conference on Interactive Theorem Proving, 2023
  2. 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
  3. Nominal Equational Problems
    In Foundations of Software Science and Computation Structures, Mar 2021