On formalised proofs of termination of recursive functions

DOI10.1007/10704567_2MaRDI QIDQ4494365zbMATH OpenFDO

Authors Fairouz Kamareddine, F. Monin

Publication date 10 August 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10704567_2

zbMATH Keywords

proof checkersProPre systemtheorem provers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• An ordinal measure based procedure for termination of functions
• scientific article; zbMATH DE number 1500561
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
• Toward automating the discovery of decreasing measures
• Termination analysis for functional programs

Cited in

(9)

• Proving termination of normalization functions for conditional expressions
• Automatizing termination proofs of recursively defined functions
• Termination Proofs for Recursive Functions in FoCaLiZe
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
• On the Computational Content of Termination Proofs
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• scientific article; zbMATH DE number 88985 (Why is no real title available?)
• On automating the extraction of programs from proofs using product types
• An ordinal measure based procedure for termination of functions

Describes a project that uses

Uses Software

• Coq

This page was built for publication: On formalised proofs of termination of recursive functions

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