@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},}
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
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.
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.
short
An Investigation into General Nominal Equational Problems
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.
@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},}
master thesis
Nominal Disunification
Deivid Vale
University of Brasilia, Defended on july 26th 2019
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},}