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’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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abel, A., Altenkirch, T.: A predicative analysis of structural recursion. J. Funct. Program. 12(1), 1–41 (2002)
Balaa, A., Bertot, Y.: Fix-point equations for well-founded recursion in type theory. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 1–16. Springer, Heidelberg (2000)
Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Hagiya, M. (ed.) FLOPS 2006. LNCS, vol. 3945, pp. 114–129. Springer, Heidelberg (2006)
Bertot, Y., Komendantsky, V.: Fixed point semantics and partial recursion in Coq. In Proceedings of PPDP 2008, Valencia, Spain, pp. 89–96 (2008)
Bonichon, R., Delahaye, D., Doligez, D.: \(\sf Zenon\): an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. LNCS, vol. 4790, pp. 151–165. Springer, Heidelberg (2007)
Boulmé, S., Hardin, T., Hirschkoff, D., Ménissier-Morain, V., Rioboo, R.: On the way to certify computer algebra systems. In: Proceedings of the Calculemus Workshop of FLOC 1999. ENTCS, vol. 23. Elsevier (1999)
Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers an overview. Math. Struct. Comput. Sci. FirstView, 1–51 (2015)
Bulwahn, L., Krauss, A., Nipkow, T.: Finding lexicographic orders for termination proofs in Isabelle/HOL. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 38–53. Springer, Heidelberg (2007)
Bury, G., Delahaye, D.: Integrating simplex with tableaux. In: Nivelle, H.D. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods. LNCS, vol. 9323, pp. 86–101. Springer, Heidelberg (2015)
Dubois, C., Hardin, T., Donzeau-Gouge, V.: Building certified components within FOCAL. Trends in Functional Programming, vol. 5, pp. 33–48 (2006)
Hyvernat, P.: The Size-change termination principle for constructor based languages. Logical Methods Comput. Sci. 10(1) (2014)
Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 460–475. Springer, Heidelberg (2007)
Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303–336 (2010)
Lamport, L.: How to write a proof. Research report, Digital Equipment Corporation (1993)
Pessaux, F.: Focalize: Inside an F-IDE. In: Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014. EPTCS, vol. 149, pp. 64–78 (2014)
Prevosto, V.: Conception et Implantation du langage FoC pour le développement de logiciels certifiés. Ph.D. thesis, Université Paris 6, September 2003
Slind, K.: Another look at nested recursion. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 498–518. Springer, Heidelberg (2000)
Acknowledgements
We thank Renaud Rioboo for the useful discussions and case studies. Thanks to Julien Forest for the helpful discussions about Function. Lastly we thank William Bartlett for his work on a very first prototype.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Dubois, C., Pessaux, F. (2016). Termination Proofs for Recursive Functions in FoCaLiZe . In: Serrano, M., Hage, J. (eds) Trends in Functional Programming. TFP 2015. Lecture Notes in Computer Science(), vol 9547. Springer, Cham. https://doi.org/10.1007/978-3-319-39110-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-39110-6_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-39109-0
Online ISBN: 978-3-319-39110-6
eBook Packages: Computer ScienceComputer Science (R0)