Le but de cet exposé est de connecter la culture des évaluateurs (McCarthy; Reynolds; Steele et Sussman; Greussay; Wadler; etc.) et celle des machines abstraites (Landin; Krivine; Felleisen et al.; Curien, Cousineau et Mauny; Hannan et Miller; etc.) pour le lambda-calcul. Cette connection est basée sur quelques transformations de programme simples: représenter les valeurs expressibles et dénotables par des fermetures, matérialiser le flot de contrôle de l'évaluateur avec des continuations, et défunctionaliser ces continuations (optionnellement, on peut aussi introduire une pile de données intermédiaires).
Les résultats de cette connection sont assez sidérants: par exemple, à partir du plus canonique des évaluateurs du lambda-calcul, on peut obtenir et la machine de Krivine, et la CEK-machine; la seule différence est que l'une est obtenue en passant des continuations avec appel par nom, et l'autre avec appel par valeur. L'évaluateur lui est unique — mais il dépend de l'ordre d'évaluation de son méta-language, comme nous en avait averti John Reynolds dans « Definitional Interpreters for Higher-Order Programming Languages », il y a plus de 30 ans.
Avec cette connection sous le bras, on peut revisiter les classiques, et montrer par exemple que la machine SECD correspond à un évaluateur compositionnel avec un environnement, une stratégie « callee-save », et un délimiteur de contrôle.
On peut aussi construire des machines abstraites pour des effets calculatoires arbitraires, en partant d'un évaluateur monadique et d'une monade donnée.
Dans le domaine de la sécurité, on peut même spécifier l'inspection de pile (« stack inspection ») dans des évaluateurs et des machines abstraites arbitraires, et le faire d'une manière qui respecte la récursivité terminale, en construisant sur les resultats de Clements et Felleisen présentés à ESOP 2003.
Plutôt que des fonctions d'évaluation, on peut aussi considérer des fonctions de normalisation (cf. la normalisation par évaluation) et mécaniquement construire les machines abstraites correspondantes.
On peut enfin appliquer la correspondance à d'autres langages que le lambda-calcul, comme Featherweight Java, mini-Smalltalk, une version propositionnelle de Prolog avec CUT, etc.
Cette correspondence entre évaluateurs et machines abstraites peut servir de méthodologie pour révéler le contenu dénotationnel d'une machine abstraite et aussi pour extraire le contenu opérationnel d'une function d'évaluation.