Translating proofs from Lean to Dedukti

Traduction de preuves de Lean vers Dedukti Cette thèse traite de la traduction de preuves de l'assistant de démonstration Lean vers le cadre logique Dedukti. Partant d'une interprétation de base de Lean en tant que variante d'un système de types pur et d'un encodage Dedukti correspondant, nous décrivons l'encodage des différentes égalités définitionnelles de Lean dans Dedukti, en accordant une attention particulière au jugement d'équivalence de Lean sur les termes de niveau univers à la lumière du type propositionnel imprédicatif et du polymorphisme d'univers prenex de Lean. Comme toutes les égalités définitionnelles de Lean ne sont pas directement encodables dans Dedukti, nous recourons à une étape de pré-traduction au cours de laquelle nous éliminons diverses égalités définitionnelles en adaptant une traduction générale de la théorie des types extensionnelle vers la théorie des types intensionnelle. De plus, nous rendons compte des aspects pratiques du développement d’une telle traduction, en décrivant un certain nombre d’optimisations qui ont été mises en œuvre, et identifions les principaux défis restants liés à l’adaptation de la traduction à des entrées plus volumineuses. Nous décrivons également certaines perspectives d'avenir associées à nos travaux, avec des implications possibles pour les développements futurs du noyau et de la métathéorie de Lean.