Formal Verification of Termination Criteria for First-Order Recursive Functions

César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, Thiago Mendonça Ferreira Ramos. Formal Verification of Termination Criteria for First-Order Recursive Functions. In Liron Cohen 0001, Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). Volume 193 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [doi]

@inproceedings{MunozAMDNAAR21,
  title = {Formal Verification of Termination Criteria for First-Order Recursive Functions},
  author = {César A. Muñoz and Mauricio Ayala-Rincón and Mariano M. Moscato and Aaron Dutle and Anthony J. Narkawicz and Ariane Alves Almeida and Andréia B. Avelar and Thiago Mendonça Ferreira Ramos},
  year = {2021},
  doi = {10.4230/LIPIcs.ITP.2021.27},
  url = {https://doi.org/10.4230/LIPIcs.ITP.2021.27},
  researchr = {https://researchr.org/publication/MunozAMDNAAR21},
  cites = {0},
  citedby = {0},
  booktitle = {12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  editor = {Liron Cohen 0001 and Cezary Kaliszyk},
  volume = {193},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-188-7},
}