A. Ayad and C. Marché, Behavioral properties of floating-point programs. Hisseo publications, 2009.

J. Filliâtre, Why: a multi-language multi-prover verification tool, Research Report, vol.1366, issue.11, 2003.

F. Bobot, S. Conchon, É. 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, 2008.
DOI : 10.1145/1512464.1512466

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

. Ph and . Wadler, Efficient Compilation of Pattern Matching The Implementation of Functional Programming Languages, chapter 6, INRIA Centre de recherche INRIA Saclay ? Île-de-France Parc Orsay Université -ZAC des Vignes 4, rue Jacques Monod -91893 Orsay Cedex, 1987.