Abstract
This paper presents the formal verification with the Coq proof assistant of several applicative data structures implementing finite sets. These implementations are parameterized by an ordered type for the elements, using functors from the ML module system. The verification follows closely this scheme, using the newly Coq module system. One of the verified implementation is the actual code for sets and maps from the Objective Caml standard library. The formalization refines the informal specifications of these libraries into formal ones. The process of verification exhibited two small errors in the balancing scheme, which have been fixed and then verified. Beyond these verification results, this article illustrates the use and benefits of modules and functors in a logical framework.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
The Coq Proof Assistant, http://coq.inria.fr/
The Objective Caml language, http://caml.inria.fr/
Adams, S.: Functional pearls: Efficient sets – a balancing act. Journal of Functional Programming 3(4), 553–561 (1993); Expanded version available as Technical Report CSTR 92-10, University of Southampton
Adel’son-Vel’skiĭ, G.M., Landis, E.M.: An algorithm for the organization of information. Soviet Mathematics–Doklady 3(5), 1259–1263 (1962)
Chrząszcz, J.: Implementing modules in the system Coq. In: 16th International Conference on Theorem Proving in Higher Order Logics, University of Rome III (September 2003)
Chrząszcz, J.: Modules in Type Theory with generative definitions. PhD thesis, Warsaw University and Université Paris-Sud (2003); To be defended
Courant, J.: A Module Calculus for Pure Type Systems. In: Typed Lambda Calculi and Applications 1997. LNCS, pp. 112–128. Springer, Heidelberg (1997)
Guibas, L.J., Sedgewick, R.: A dichromatic framework for balanced trees. In: 19th Annual Symposium on Foundations of Computer Science, Ann Arbor, Michigan, October 16-18, pp. 8–21. IEEE, Los Alamitos (1978)
Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: Conference record of POPL 1994: 21st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Portland, OR, January 1994, pp. 123–137 (1994)
Hinze, R.: Constructing red-black trees. In: Okasaki, C. (ed.) Proceedings of the Workshop on Algorithmic Aspects of Advanced Programming Languages, WAAAPL 1999, Paris, France, September 1999, pp. 89–99 (1999); Also technical report of Columbia University, CUCS-023-99
Leroy, X.: A modular module system. Journal of Functional Programming 10(3), 269–303 (2000)
Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg (2003)
Letouzey, P.: Programmation fonctionnelle certifiée en Coq. PhD thesis, Universit é Paris Sud (2003); To be defended
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)
Wadler, P.: Deforestation: transforming programs to eliminate trees. Theoretical Computer Science 73, 231–248 (1990)
Xi, H.: Dependently Typed Data Structures. In: Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL 1999), Paris, September 1999, pp. 17–32 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Filliâtre, JC., Letouzey, P. (2004). Functors for Proofs and Programs. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive