Olivier Danvy (Brics, Aarhus, Danemark)

Comment est-ce que l’on spécifie l’exécution d’un programme? Certains utilisent un systeme de calcul, e.g., le lambda-calcul. Certains autres utilisent une machine abstraite, i.e., des transitions entre états. D’autres encore utilisent une fonction d’évaluation, i.e., un interprète. D’autres enfin utilisent un compilateur vers un code octal (``byte code’’) et une machine virtuelle qui opère sur ce code.

Comment est-ce que l’on vérifie que les artéfacts sémantiques mentionnés ci- dessus sont mutuellement compatibles? Par exemple, comment est-ce que l’on vérifie qu’un processeur de code implémente un calcul correctement? Et plus généralement, comment est-ce que l’on conçoit de tels artéfacts sémantiques?

C’est notre thèse (*) que dans beaucoup de cas intéressants, ces artéfacts sémantiques peuvent être dérivés les uns des autres, et de plus, que ces artéfacts sont basées sur des transformations de programme qui sont très simples. Une technique dite de ``refocus’’ permet d’aller de la réduction à un pas induite par un calcul vers une machine abstraite (correspondence syntaxique). Une combinaison de la transformation en CPS et de la défonctionalisation permet d’aller d’un interprète vers une machine abstraite (correspondence fonctionnelle). Cette approche dérivationnelle permet de connecter calculs et fonctions d’évaluation, de reconstruire des machines abstraites qui ont été indépendemment conçues et d’en construire de nouvelles. En sus, nous effleurerons en passant les compilateurs et les machines virtuelles.

(*) «http://www.brics.dk/~danvy/DSc.html»