a:2:{s:2:"fr";s:622:"Depuis 2003, d'abord dans le cadre de l'ARC Concert, puis actuellement dans le cadre du projet Compcert, je m'intéresse à l'utilisation des méthodes formelles pour spécifier et certifier un compilateur C, à l'aide de l'assistant à la preuve Coq. Cela nécessite de définir à différents niveaux d'abstraction des sémantiques formelles des langages du compilateur, et de prouver ensuite sur machine des propriétés de correction de ces sémantiques. Auparavant, j'ai utilisé l'évaluation partielle dans le but de faciliter la compréhension et la maintenance d'applications scientifiques écrites en Fortran. ";s:2:"en";s:622:"Depuis 2003, d'abord dans le cadre de l'ARC Concert, puis actuellement dans le cadre du projet Compcert, je m'intéresse à l'utilisation des méthodes formelles pour spécifier et certifier un compilateur C, à l'aide de l'assistant à la preuve Coq. Cela nécessite de définir à différents niveaux d'abstraction des sémantiques formelles des langages du compilateur, et de prouver ensuite sur machine des propriétés de correction de ces sémantiques. Auparavant, j'ai utilisé l'évaluation partielle dans le but de faciliter la compréhension et la maintenance d'applications scientifiques écrites en Fortran. ";}