Termination Proofs for Recursive Functions in FoCaLiZe
| Autor: | François Pessaux, Catherine Dubois |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Functional programming
Theoretical computer science Programming language Computer science computer.file_format Construct (python library) computer.software_genre Mathematical proof Formal proof Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Glue code Executable Compiler computer |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319391090 TFP |
| DOI: | 10.1007/978-3-319-39110-6_8 |
| Popis: | 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 Coqi¾źwe rely on the Coq construct Function. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|