Retour à l'index du GREYC

Séminaire Algorithmique

Site du CNRS

Séminaire Algorithmique

Le séminaire a lieu le mardi à 11 h 45 (sauf modification exceptionnelle), au campus Côte de Nacre, bâtiment Sciences 3, salle S3 351, 3ème étage.

Résumé du séminaire du Mardi 12 Décembre 2006 à 14:00

Les machines abstraites pour langages d'ordre supérieur

par 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>

GREYC
Campus Côte de Nacre, boulevard du Maréchal Juin
BP 5186
14032 Caen Cedex
FAX : +33 (0)2 31 56 73 30
http://www.greyc.fr