Chercher les représentations canoniques des programmes – REPRO

Le projet REPRO vise à: - Approfondir notre compréhension de la structure des programmes informatiques en découvrant des représentations canoniques de programmes, - Explorer leurs applications aux problèmes d'équivalence et de synthèse de programmes. Une représentation canonique est une façon différente de représenter un programme qui capture mieux leur identité : deux formes canoniques différentes correspondent à deux programmes au comportement différent. Nous savons peu de choses des représentations canoniques, à part dans des cas idéalisés restreints (le lambda-calcul simplement typé). Le projet REPRO propose d'étudier les formes canoniques de langages de programmation, en particulier les langagesfonctionnels fortement typés. Cela demande de nouveaux développements théoriques, et pourrait avoir de nombreuses applications pour décider l'équivalence de programmes (vérifier un refactoring) ou la synthèse de programme (deviner le code à partir d'une spécification partielle).