A. Ayad and C. Marché, Multi-Prover Verification of Floating-Point Programs, Fifth International Joint Conference on Automated Reasoning, 2010.
DOI : 10.1007/978-3-642-14203-1_11
URL : https://hal.archives-ouvertes.fr/inria-00534333

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Bobot, S. Conchon, E. Contejean, and S. Lescuyer, Implementing polymorphism in SMT solvers, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, pp.1-5, 2008.
DOI : 10.1145/1512464.1512466

S. Conchon and E. Contejean, The Alt-Ergo automatic theorem prover, APP deposit under the number, 2008.

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

C. Okasaki, Purely Functional Data Structures, 1998.
DOI : 10.1017/CBO9780511530104

A. Paskevich, Algebraic types and pattern matching in the logical language of the Why verification platform, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00439232

N. Shankar and P. Mueller, Verified Software: Theories, Tools and Experiments (VSTTE'10) Software Verification Competition, 2010.