Raisonner et Programmer avec des Données Infinies – RAPIDO

Rapido a pour objectif de rassembler de jeunes chercheurs de manière à étudier la possibilité d'appliquer des méthodes issues de la théorie de la démonstration pour raisonner et programmer avec des structures infinies.

Le but du projet est, d'un point de vue fondamental :
- de développer des systèmes logiques à même de capturer des preuves infinies (systèmes de preuves avec plus petits et plus grands points fixes mais également systèmes de preuves infinitaires),
- de concevoir et d'étudier des langages de programmation pour la manipulation de données infinies aussi bien d'un point de vue sémantique que syntaxique.

En outre, l'ambition du projet est d'appliquer les résultats fondamentaux qui auront été obtenus lors des recherches ci-dessus en vue :
(i) de développer des outils logiciels dédiés au raisonnement sur les programmes calculant sur les données infinis (comme les streams ou plus généralement les programmes coinductifs), et
(ii) d'étudier les propriétés des automates sur les mots et les arbres infinis d'un point de vue preuve-théorique, avec un œil vers les problèmes de model-checking.