Termination Proofs for Recursive Functions in FoCaLiZe

DOI10.1007/978-3-319-39110-6_8zbMath1338.68240OpenAlexW2461166840MaRDI QIDQ2814388

François Pessaux, Catherine Dubois

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

recursionterminationfunctional programmingformal proofCoqFoCaLiZe

Mathematics Subject Classification ID

Related Items (2)

ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti ⋮ Modular verification of programs with effects and effect handlers in Coq

Uses Software

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

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