Formal verification of termination criteria for first-order recursive functions
From MaRDI portal
Publication:6149593
DOI10.1007/S10817-023-09669-ZOpenAlexW3174648313MaRDI QIDQ6149593FDOQ6149593
Authors: César Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andréia B. Avelar da Silva, Thiago Mendonça Ferreira Ramos 
Publication date: 6 February 2024
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-023-09669-z
Cites Work
- Termination of Isabelle functions via termination of rewriting
- Introduction to algorithms.
- Title not available (Why is that?)
- The size-change principle for program termination
- An axiomatic basis for computer programming
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Certified Size-Change Termination
- Title not available (Why is that?)
- Termination Analysis with Calling Context Graphs
- Enumeration of the Elementary Circuits of a Directed Graph
- Title not available (Why is that?)
- The size-change principle and dependency pairs for termination of term rewriting
- Formalization of the undecidability of the halting problem for a functional language
- Formalization of the computational theory of a Turing complete functional language model
- Title not available (Why is that?)
This page was built for publication: Formal verification of termination criteria for first-order recursive functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149593)
