Raisonner avec des preuves circulaires pour la programmation – RECIPROG
ReCiProg est un projet collaboratif (Lyon-Marseille-Nantes-Paris) qui a pour but de construire d'étendre la correspondance preuves-programmes (dite correspondance de Curry-Howard) aux programmes récursifs et aux preuves circulaires pour des logiques et systèmes de types utilisants l'induction et la coinduction. Le projet contribuera aussi bien au développement des fondements théoriques nécessaires relatifs aux preuves circulaires qu'au développement logiciel permettant d'améliorer l'utilisation des types coinductifs et du raisonnement par coinduction dans l'assistant de preuves Coq qui présente, dans l'état de l'art, d'importants défauts auxquels le projet vise à remédier.
Coordination du projet
Alexis Saurin (Institut de Recherche en Informatique Fondamentale)
L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.
Partenariat
IRIF Institut de Recherche en Informatique Fondamentale
LS2N Laboratoire des Sciences du Numérique de Nantes
LIP - CNRS Laboratoire d'Informatique du Parallélisme
LIS Laboratoire d'Informatique et Systèmes
Aide de l'ANR 456 182 euros
Début et durée du projet scientifique :
septembre 2021
- 48 Mois
