On Solving Nominal Disunification Constraints. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Deivid Vale (LSFA, 2019)

An Investigation into General Nominal Equational Problems (Work in progress). - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Deivid Vale (UNIF, 2020)

Nominal Equational Problems. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Deivid Vale (FoSSaCS, 2021)

Tuple Interpretations for Higher-Order Complexity. - Cynthia Kop; Deivid Vale (FSCD, 2021)

Tuple Interpretations for Higher-Order Rewriting. - Deivid Vale; Cynthia Kop (CoRR, 2021)

Formalizing Higher-Order Termination in Coq. - Deivid Vale; Niels van der Weide (CoRR, 2021)

Tuple Interpretations and Applications to Higher-Order Runtime Complexity. - Cynthia Kop; Deivid Vale (CoRR, 2022)

Analyzing Innermost Runtime Complexity Through Tuple Interpretations. - Liye Guo; Deivid Vale (LSFA, 2022)

Cost-Size Semantics for Call-By-Value Higher-Order Rewriting. - Cynthia Kop; Deivid Vale (FSCD, 2023)

Certifying Higher-Order Polynomial Interpretations. - Niels van der Weide; Deivid Vale; Cynthia Kop (ITP, 2023)

Complexity Analysis for Call-by-Value Higher-Order Rewriting. - Cynthia Kop; Deivid Vale (CoRR, 2023)

On Basic Feasible Functionals and the Interpretation Method. - Patrick Baillot; Ugo Dal Lago; Cynthia Kop; Deivid Vale (FoSSaCS (2), 2024)

Higher-Order Constrained Dependency Pairs for (Universal) Computability. - Liye Guo; Kasper Hagens; Cynthia Kop; Deivid Vale (MFCS, 2024)