Micaela Mayero

      

Contacts:

LIPN - UMR CNRS 7030
Institut Galilée - Université Paris Nord
99 avenue Jean-Baptiste Clément
93430 Villetaneuse
FRANCE

Tél.
Fax
: +33 (0) 1 49 40 36 91
: +33 (0) 1 48 26 07 12
Micaela.Mayero [at] lipn.univ-paris13.fr
Bureau
: A209


English version

Last modified: Thu Mar 21 17:15:49 CEST 2024
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 7030PPS, CNRS UMR 7126
Université Paris13Université Paris 7
99 avenue Jean-Baptiste Clément175 Rue du Chevaleret
93430 VILLETANEUSEPARIS 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 LATEX par HEVEA