Automatizing termination proofs of recursively defined functions
From MaRDI portal
Publication:1346629
DOI10.1016/0304-3975(94)00021-2zbMath0829.68031OpenAlexW1990295079MaRDI QIDQ1346629
Pascal Manoury, Marianne Simonot
Publication date: 6 April 1995
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(94)00021-2
Related Items
A user's friendly syntax to define recursive functions as typed λ-terms ⋮ Automating inversion of inductive predicates in Coq ⋮ AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS ⋮ On automating the extraction of programs from proofs using product types ⋮ An ordinal measure based procedure for termination of functions
Cites Work
This page was built for publication: Automatizing termination proofs of recursively defined functions