publications

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, August 26-30, 2024, Bratislava, Slovakia, 2024

   DOI

2023

1. 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
   }

2. 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
3. short

   Nijn/Onijn: A New Certification Engine for Higher-Order Termination

   Cynthia Kop, Deivid Vale, and Niels van der Weide

   In Proc. 11th International Workshop on Higher-Order Rewriting, Jul 2023

   PDF Slides

2022

1. conf

   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, Jul 2022

   DOI
2. short

   Tuple Interpretations and Applications to Higher-Order Runtime Complexity

   Cynthia Kop, and Deivid Vale

   In Proc. 18th International Workshop on Termination, Jun 2022

   arXiv PDF

2021

1. 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
2. conf

   Tuple Interpretations for Higher-Order Complexity

   Cynthia Kop, and Deivid Vale

   In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Jul 2021

   DOI arXiv
3. short

   Nominal Disunification via Fixed-Point Constraints

   Leonardo M. Batista, Maribel Fernández, Daniele Nantes-Sobrinho, and 1 more author

   In Proc. 35th International Workshop on Unification, Jul 2021

   PDF
4. short

   Formalizing Higher-Order Termination in Coq

   Deivid Vale, and Niels Weide

   In Proc. 17th International Workshop on Termination, May 2021

   Abs arXiv Code

   We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type theory. Using this formalization, one can implement several termination techniques, like the interpretation method or dependency pairs, and prove their correctness. Those implementations can then be extracted to OCaml, which results in a verified termination checker.

2020

1. short

   Tuple Interpretations for Higher-Order Rewriting

   Cynthia Kop, and Deivid Vale

   In Proc. 22th Intertational Workshop on Logic and Computational Complexity, Jun 2020

   Abs PDF Website

   We present a style of algebra interpretations for many-sorted and higher-order term rewriting based on interpretations to tuples; intuitively, a term is mapped to a sequence of values identifying for instance its evaluation cost, size and perhaps other values. This could give a more finegrained notion of the complexity of a term or TRS than notions such as runtime or derivational complexity.

2. short

   An Investigation into General Nominal Equational Problems

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

   In Proc. 34th International Workshop on Unification, Jun 2020

   Abs PDF Website

   This workshop paper presents novel research ideas for a nominal treatment of nominal equational problems. We discuss some issues of such specification and give a first glimpse of a natural rule-based system to work with this problem. In a specific way, this extends what we have done before on disunification constraints by allowing explicit existential and universal quantification to unknowns.

2019

1. conf

   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, Jun 2019

   DOI Bib

   @inproceedings{ayala:fernandez:nantes:vale:19,
     author = {Ayala{-}Rinc{\'{o}}n, Mauricio and Fern{\'{a}}ndez, Maribel and Nantes{-}Sobrinho, Daniele and Vale, Deivid},
     editor = {Felty, Amy P. and Marcos, Jo{\~{a}}o},
     title = {On Solving Nominal Disunification Constraints},
     booktitle = {Proceedings of the 14th Workshop on Logical and Semantic Frameworks with Applications, {LSFA} 2019, Natal, Brazil},
     series = {Electronic Notes in Theoretical Computer Science},
     volume = {348},
     pages = {3--22},
     publisher = {Elsevier},
     year = {2019},
     url = {https://doi.org/10.1016/j.entcs.2020.02.002},
     doi = {10.1016/j.entcs.2020.02.002},
     timestamp = {Tue, 16 Aug 2022 23:04:31 +0200},
     biburl = {https://dblp.org/rec/conf/lsfa/Ayala-RinconFNV20.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     bibtex_show = true
   }

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
   }