Cette thèse propose une nouvelle logique d'arbres finis pour analyser les programmes manipulant les données du Web. Cette logique offre le meilleur compromis connu entre expressivité et complexité. Elle est aussi expressive que la logique monadique du second ordre (l'une des logiques les plus expressives qu'on connaît, prouvée décidable en 1969 en temps hyperexponentiel), tout en étant décidable en temps simplement exponentiel. Elle a fourni le premier système de type statique pour le langage standard de requêtes XPath, et le premier logiciel capable d'analyser efficacement les types de données du Web et les requêtes sur ces données, ce qu'on pensait hors de portée.
