Vérifier des fonctions d'ordre supérieur à l'aide d'automates d'arbre

Les fonctions d'ordre superieur font partie integrante des langages de program-mation modernes comme Haskell, Caml, mais aussi Java, Scala ou meme JavaS-cript. La ou leur utilite n'est plus a demontrer, leur utilisation pose probleme des lors qu'il s'agit de prouver la correction des programmes qui les utilisent. Dans ce travail, nous proposons une methode de verification basee sur les systemes de reecriture de termes et les automates d'arbre.