publications

2026

1. A Nominal Approach to Equational Problems in Languages with Binders

   Daniele Nantes-Sobrinho, Maribel Fernández, Deivid Vale, and 1 more author

   ACM Trans. Comput. Log., 2026

   DOI

2025

1. A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations

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

   Log. Methods Comput. Sci., 2025

   DOI

2024

1. 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
2. Higher-Order Constrained Dependency Pairs for (Universal) Computability

   Liye Guo, Kasper Hagens, Cynthia Kop, and 1 more author

   In 49th International Symposium on Mathematical Foundations of Computer Science, MFCS 2024, Bratislava, Slovakia, August 26-30, 2024, 2024

   DOI
3. On Basic Feasible Functionals and the Interpretation Method

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

   CoRR, 2024

   DOI
4. Higher-Order Constrained Dependency Pairs for (Universal) Computability

   Liye Guo, Kasper Hagens, Cynthia Kop, and 1 more author

   CoRR, 2024

   DOI

2023

1. 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, Rome, Italy, July 3-6, 2023, 2023

   DOI
2. Certifying Higher-Order Polynomial Interpretations

   Niels Weide, Deivid Vale, and Cynthia Kop

   In 14th International Conference on Interactive Theorem Proving, ITP 2023, Białystok, Poland, July 31 - August 4, 2023, 2023

   DOI
3. Certifying Higher-Order Polynomial Interpretations

   Niels Weide, Deivid Vale, and Cynthia Kop

   CoRR, 2023

   DOI
4. Complexity Analysis for Call-by-Value Higher-Order Rewriting

   Cynthia Kop and Deivid Vale

   CoRR, 2023

   DOI

2022

1. Analyzing Innermost Runtime Complexity Through Tuple Interpretations

   Liye Guo and Deivid Vale

   In Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2022, Belo Horizonte, Brazil (hybrid), 23-24 September 2022, 2022

   DOI
2. Tuple Interpretations and Applications to Higher-Order Runtime Complexity

   Cynthia Kop and Deivid Vale

   CoRR, 2022

   DOI

2021

1. 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 - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, 2021

   DOI
2. Tuple Interpretations for Higher-Order Complexity

   Cynthia Kop and Deivid Vale

   In 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, Buenos Aires, Argentina (Virtual Conference), July 17-24, 2021, 2021

   DOI
3. Tuple Interpretations for Higher-Order Rewriting

   Deivid Vale and Cynthia Kop

   CoRR, 2021
4. Formalizing Higher-Order Termination in Coq

   Deivid Vale and Niels Weide

   CoRR, 2021

2020

1. An Investigation into General Nominal Equational Problems (Work in progress)

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

   In Proceedings of the 34th International Workshop on Unification, UNIF 2020, Linz, Austria, June 29, 2020, 2020

2019

1. On Solving Nominal Disunification Constraints

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

   In Proceedings of the 14th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2019, Natal, Brazil, August, 2019, 2019

   DOI
2. master thesis

   Nominal Disunification

   Deivid Vale

   University of Brasilia, Defended on july 26th 2019

   Abs Bib PDF

   My master thesis’s research was all about solving nominal disunification problems. The nominal setting is a very nice formalism to deal with alpha-equivalence. It’s also very usefull to deal with name-scoping in programming languages and to have a formal proof that under suitable context assumptions I can call all my friends by just ’José’ :)

   @mastersthesis{deivid:2019,
     author = {Vale, Deivid},
     school = {University of Brasilia},
     title = {Nominal Disunification},
     month = {Defended on July 26th},
     year = {2019},
     bibtex_show = true
   }