stage_coqreals
Sujet de stage
Une bibliothèque réelle unifiée pour Coq
Encadrement : Micaela Mayero
Lieu principal:
équipe LCR
LIPN, CNRS UMR 7030
Université Paris13
99 avenue Jean-Baptiste Clément
93430 VILLETANEUSE
Contacts : Micaela.Mayero [@] lipn.univ-paris13.fr
Financement : oui
Objectif du stage:
Il existe plusieurs bibliothèques de nombres réels dans Coq et de
nombreux travaux ont été et sont encore menés sur la formalisation des
nombres réels dans Coq. Ce stage concerne les deux principales
bibliothèques, la bibliothèque standard classique “Reals” [Coq] et la
bibliothèque intuitionniste “CoRN” [CoRN]. Une étude de ces deux
bibliothèques a été faite par leurs auteurs (Mayero-Niqui) afin de
développer une unique bibliothèque des nombres réels qui comprendrait
une partie commune [MM-HDR]. Le but de ce stage est de poursuivre cette
étude, dont les conclusions ne sont pas figées, ainsi que le
développement (un prototype existe).
Ce sujet requiert une bonne connaissance de Coq, de la théorie des
types, du calcul des construction inductives et de l’analyse réelle
classique et intuitionniste.
Ce sujet pourra également aborder la problématique de l’extraction de
programme [EXTRACT] et de la réalisabilité classique [AM-HDR].
Remarques : Collaboration avec Bas Spitters:
http://www.cs.ru.nl/ spitters/
Séjours à Nijmegen (Pays-Bas) possibles.
Le sujet peut être étendu pour une éventuelle poursuite en thèse.
Prérequis: une connaissance de Coq sera appréciée.
Références
-
[Coq]
-
The Coq proof assistant.
http://coq.inria.fr.
- [CoRN]
-
The CoRN reference.
http://corn.cs.ru.nl/.
- [MM-HDR]
-
M.Mayero. Manuscrit d’habilitation à diriger des
recherches. 2012..
- [EXTRACT]
-
L. Cruz-Filipe and P. Letouzey..
A Large-Scale Experiment in
Executing Extracted Programs. Calculemus 2005.
- [AM-HDR]
-
A.Miquel. Manuscrit d’habilitation à diriger des
recherches. 2009..
Ce document a été traduit de LATEX par HEVEA
