Automatizing termination proofs of recursively defined functions

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

zbMATH Keywords

ProPRe program synthesis system

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theory of software (68N99)

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

• Recursive programming with proofs
• Unnamed Item
• Unnamed Item

This page was built for publication: Automatizing termination proofs of recursively defined functions