Termination Proofs for Recursive Functions in FoCaLiZe

摘要

FoCaLiZe is a development environment allowing the writing of specifications, implementations and correctness proofs. It generates both OCaml (executable) and Coq code (for verification needs). This paper extends the language and the compiler to handle termination proofs relying on well-founded relations or measures. We propose an approach where the user's burden is lightened as much as possible, leaving glue code to the compiler. Proofs are written using the declarative proof language provided by FoCaLiZe, and the automatic theorem prover Zenon. When compiling to Coq we rely on the Coq construct Function.