Micaela Mayero Homepage

stage_cerpan_extraction

Sujet de stage
Une extraction en Coq pour les nombres réels et flottants?

Encadrement : Micaela Mayero, Pierre Letouzey

Lieu principal:	Autre lieu:
équipe LCR
LIPN, CNRS UMR 7030	PPS, CNRS UMR 7126
Université Paris13	Université Paris 7
99 avenue Jean-Baptiste Clément	175 Rue du Chevaleret
93430 VILLETANEUSE	PARIS 13e

Contacts : Micaela.Mayero [@] lipn.univ-paris13.fr

Financement : oui
Objectif du stage:
De récents travaux [CFL05] ont été fait sur une formalisation constructive des réels [GN02]. Nous nous intéressons à la formalisation de problèmes numériques utilisant les flottants et réels classiques. Le principe d’extraction de Coq ne traite pas la famille des nombres réels ni celle des flottants, et ce stage consiste à voir comment étendre l’extraction vers cette famille. Une piste pourraît être l’étude de la réalisabilité de certains axiomes de la librairie standard des réels (Reals) par un développement existant des réels exacts [Dig] (par exemple).
Prérequis: une connaissance de Coq sera appréciée.

Références

[CFL05]: L. Cruz-Filipe and P. Letouzey. A Large-Scale Experiment in Executing Extracted Programs. In 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus’2005, 2005.
[Dig]: http://homepages.cwi.nl/~milad/manydigits/exact_contents.html.
[GN02]: Herman Geuvers and Milad Niqui. Constructive reals in Coq: Axioms and categoricity. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Types for Proofs and Programs : International Workshop, TYPES 2000, Durham, UK, December 8–12, 2000. Selected Papers, volume 2277 of Lecture Notes in Computer Science, pages 79–95. Springer-Verlag, 2002.

Ce document a été traduit de L^AT_EX par H^EV^EA