Les machines abstraites et compilateurs natifs pour les langages
fonctionnels implémentent efficacement la réduction faible du
lambda-calcul (on ne réduit pas sous les lambdas). Des applications
comme l'évaluation partielle et le test de convertibilité des
assistants de preuves comme Coq nécessitent cependant la réduction forte
(on réduit sous les lambdas jusqu'à la forme normale).
Dans cet exposé, nous montrerons comment un réducteur faible efficace
(la machine abstraite Zinc d'Objective Caml) peut être modifié de
manière minimale afin d'effectuer la réduction forte ou le test de
convertibilité. Une implémentation de cette machine abstraite pour la
réduction forte dans le système Coq, ainsi qu'une preuve Coq de la
correction de la machine et de son compilateur, sont en cours.