An ordinal measure based procedure for termination of functions

DOI10.1016/S0304-3975(99)00118-8zbMath0972.68143OpenAlexW2076897476WikidataQ126815399 ScholiaQ126815399MaRDI QIDQ5940917

Marianne Simonot, François Monin

Publication date: 20 August 2001

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(99)00118-8

zbMATH Keywords

automated program synthesis systemformal proofsNQTHMordinal measuresProPretermination

Mathematics Subject Classification ID

Related Items (3)

Size-based termination of higher-order rewriting ⋮ AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS ⋮ On automating the extraction of programs from proofs using product types

Uses Software

• Coq
• NQTHM

Cites Work

• Recursive programming with proofs
• Automatizing termination proofs of recursively defined functions
• Termination of nested and mutually recursive algorithms
• An ordinal calculus for proving termination in term rewriting
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An ordinal measure based procedure for termination of functions