A Hoare Logic for Call-by-Value Functional Programs

Yann Régis-Gianas 1 François Pottier 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We present a Hoare logic for a call-by-value programming language equipped with recursive, higher-order functions, algebraic data types, and a polymorphic type system in the style of Hindley and Milner. It is the theoretical basis for a tool that extracts proof obligations out of programs annotated with logical assertions. These proof obligations, expressed in a typed, higher-order logic, are discharged using off-the-shelf automated or interactive theorem provers. Although the technical apparatus that we exploit is by now standard, its application to functional programming languages appears to be new, and (we claim) deserves attention. As a sample application, we check the partial correctness of a balanced binary search tree implementation.
Type de document :
Communication dans un congrès
MPC 08 - Proceedings of the Ninth International Conference on Mathematics of Program Construction, Jul 2008, Marseille, France. Springer, 5133, pp.305--335, 2008, Lecture notes in computer scinece. 〈10.1007/978-3-540-70594-9_17〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00629092
Contributeur : Yann Regis-Gianas <>
Soumis le : mercredi 5 octobre 2011 - 08:49:31
Dernière modification le : vendredi 25 mai 2018 - 12:02:07

Lien texte intégral

Identifiants

Collections

Citation

Yann Régis-Gianas, François Pottier. A Hoare Logic for Call-by-Value Functional Programs. MPC 08 - Proceedings of the Ninth International Conference on Mathematics of Program Construction, Jul 2008, Marseille, France. Springer, 5133, pp.305--335, 2008, Lecture notes in computer scinece. 〈10.1007/978-3-540-70594-9_17〉. 〈inria-00629092〉

Partager

Métriques

Consultations de la notice

188