Vérification formelle d'arithmétique réelle exacte et fonctions analytiques
L'objectif de ce stage est de faire la vérification formelle de preuves
mathématiques concernant la correction d'une bibliothèque de calculs
d'arithmétique réelle exacte.
Ces calculs sont fondés sur une représentation des réels par des listes
infinies de chiffres signés d'une base quelconque,
à l'aide du principe de co-induction.