An ordinal measure based procedure for termination of functions

DOI10.1016/S0304-3975(99)00118-8MaRDI QIDQ5940917zbMATH OpenOpenAlexWikidataFDO

Authors F. Monin, M. Simonot

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

Recommendations

• scientific article; zbMATH DE number 1487841
• Algorithms for ordinal arithmetic.
• Termination analysis for functional programs
• scientific article; zbMATH DE number 1500561
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS

Cites work

• An ordinal calculus for proving termination in term rewriting
• Automatizing termination proofs of recursively defined functions
• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• scientific article; zbMATH DE number 4112064 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 3247155 (Why is no real title available?)
• Recursive programming with proofs
• Termination of nested and mutually recursive algorithms

Cited in

(7)

• Proving termination of normalization functions for conditional expressions
• Ordinal one-switch utility functions
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
• scientific article; zbMATH DE number 1487841 (Why is no real title available?)
• Size-based termination of higher-order rewriting
• On automating the extraction of programs from proofs using product types
• Algorithms for ordinal arithmetic.

Describes a project that uses

Uses Software

• Coq
• NQTHM

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5940917)