Une partie importante de la recherche en sciences du logiciel se
concentre sur la _vérification_ des programmes. J’aimerais étudier un
problème complémentaire : comment utiliser les outils formels
développés dans la communauté des langages de programmation et la
théorie de la démonstration pour _aider_ l’écriture de programmes.
Je propose trois axes d'étude principaux: la recherche de formes
_canoniques_ pour les langages avec polymorphisme en utilisant des
techniques de recherche de preuve, l'usage de procédures automatiques
de test d'équivalence de programme, et enfin la conception de systèmes
multi-langages dont certaines propriétés d'utilisabilité sont
capturées par la notion formelle de plongement _pleinement abstrait_
de langages seuls dans le système d'ensemble.