Le travail du stage s'intégrera dans l'effort de fournir une bibliothèque pour le démonstrateur Coq permettant de prouver des propriétés sur des programmes manipulants des flottants machines. Pour l'instant Coq dispose d'une librairie de base pour une représentation simple des flottants composée d'une mantisse et d'un exposant. Le but de ce stage est de compléter cette dernière pour fournir des flottants conformes au standard IEEE754.
E-mail : Laurent.Thery@sophia.inria.fr
[1] G. Huet, G. Kahn, C. Paulin-Mohring, The Coq Proof Assistant : A Tutorial : Version 6.1, Rapport Technique INRIA 0204, août 1997.
[2] Marc Daumas, Claire Finot, Laurent Théry Computer Validated Proofs of a Toolset for Adaptable Arithmetic , Rapport de Recherche INRIA 4095, Janvier 2001.
[3] David Goldberg, What Every Computer Scientist Should Know About Floating-Point Arithmetic, , ACM Computing Surveys, pp. 5-48, vol. 23#1, 1991