Termination Proofs for Recursive Functions in FoCaLiZe

DOI10.1007/978-3-319-39110-6_8MaRDI QIDQ2814388zbMATH OpenOpenAlexFDO

Authors Catherine Dubois, François Pessaux

Publication date 21 June 2016

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

Full work available at URL https://doi.org/10.1007/978-3-319-39110-6_8

zbMATH Keywords

CoqFoCaLiZeformal prooffunctional programmingrecursiontermination

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Automatizing termination proofs of recursively defined functions
• scientific article; zbMATH DE number 1487841
• scientific article; zbMATH DE number 7699444
• Termination assertions for recursive programs: Completeness and axiomatic definability
• Formalizing non-termination of recursive programs
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 2185672
• Termination analysis for functional programs
• On proving termination by innermost termination

Cited in

(5)

• Automatizing termination proofs of recursively defined functions
• Modular verification of programs with effects and effect handlers in Coq
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
• scientific article; zbMATH DE number 88985 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Zenon
• FoCaLiZe
• OCaml

This page was built for publication: Termination Proofs for Recursive Functions in FoCaLiZe

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