Towards proving the implementation of a square root algorithm in Coq/
Vers la formalisation d'un algorithme de racine carrée dans Coq
Nicolas Magaud
Projet Lemme -- INRIA Sophia-Antipolis
Collaboration avec Yves Bertot
Abstract:
We start by presenting a basic algorithm to compute square roots by hand.
We then consider an algorithm proposed by Paul Zimmermann. It is designed
to compute square roots of large numbers in an efficient manner. It relies
on the GMP library (a free library for arbitrary precision arithmetic).
We give the ideas of the algorithm and show how we intend to proceed in
order to prove its implementation correct using Coq/correctness.
Nous commencons par décrire l'algorithme de base d'extraction de racines carrées à la main.
Nous présentons ensuite un algorithme proposé par Paul Zimmermann. Cet algorithme permet
de calculer des racines carrées de grands nombres de manière efficace. Il s'appuie
sur la bibliothèque de calcul en précision arbitraire GMP.
Nous décrivons le fonctionnement de l'algorithme et montrons comment nous envisageons
de prouver la correction de son implémentation en utilisant Coq/correctness.
Back to schedule.
Nicolas Magaud
Last modified: Tue May 15 15:40:39 MEST 2001