@inproceedings{da82813472e64ec19e51be02e983a3f0,
title = "Termination proofs for recursive functions in FoCaLiZe",
abstract = "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{\textquoteright}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.",
keywords = "Coq, FoCaLiZe, Formal proof, Functional programming, Recursion, Termination",
author = "Catherine Dubois and Fran{\c c}ois Pessaux",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 16th International Symposium on Trends in Functional Programming, TFP 2015 ; Conference date: 03-06-2015 Through 05-06-2015",
year = "2016",
month = jan,
day = "1",
doi = "10.1007/978-3-319-39110-6\_8",
language = "English",
isbn = "9783319391090",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "136--156",
editor = "Manuel Serrano and Jurriaan Hage",
booktitle = "Trends in Functional Programming - 16th International Symposium, TFP 2015, Revised Selected Papers",
}