Lambda-calcul, Vérification de preuve, Assistants de preuve, Coq, Convertibilité, Réduction forte, Réduction ouverte, Évaluation paresseuse

Le test de convertibilité, qui vérifie si deux lambda-termes sont égaux à beta-réduction près, est une partie essentielle de la vérification de types et de preuves dans les assistants de preuve basés sur la théorie des types, comme Coq, Agda et Lean. Naturellement, la correction d'un tel test est nécessaire pour s'assurer que les preuves ainsi vérifiées sont valides; mais avoir un test efficace est également requis à la fois pour une interaction en temps réel avec l'utilisateur, ainsi que pour la recherche de preuve. Dans cette thèse, nous commençons par proposer une sémantique à grands pas efficace pour l'évaluation forte paresseuse, qui est l'élément critique pour implanter un test de convertibilité de manière classique. Cette sémantique est presque mécaniquement dérivée à partir de la sémantique à petits pas de réduction externe gauche du lambda-calcul, en la convertissant en sémantique à grands pas, ajoutant des environnements pour éviter les substitutions, et mémoïsant les évaluations. Des lemmes dits de transfert permettent de partager des calculs qui ne sont pas immédiatement redondants. Nous montrons ensuite comment nous pouvons améliorer cela en considérant le test de convertibilité dans sa globalité, en le voyant comme de la recherche de preuve. Pour cela, nous étudions ce qui peut être considéré comme une preuve de (non-)convertibilité, en se basant sur les travaux existants. Cela donne lieu à un nouvel algorithme parallèle et sans heuristiques, qui ne duplique pas les calculs et vient avec des garanties de complexités dans le pire des cas. Nous avons dérivé une machine virtuelle de cet algorithme, et l'avons rendue plus efficace en suivant Grégoire et Leroy, montrant que notre algorithme est adapté à la compilation des lambda-termes en entrée pour plus d'efficacité. Cette sémantique à grands pas et ce test de convertibilité parallèle ont été implémentés en OCaml et validés expérimentalement, et se révèlent significativement plus performants que Coq dans certains cas. Ils ont également été tous les deux formalisés et vérifiés en Coq, augmentant la confiance en nos travaux.