A framework for defining computational higher-order logics

Résumé : L'objectif de cette thèse est de rendre les preuves formelles plus universelles en les exprimant dans un cadre logique commun. Plus précisément nous utilisons le lambda-Pi-calcul modulo réécriture, un lambda calcul équipé de types dépendants et de réécriture, comme langage pour définir des logiques et exprimer des preuves dans ces logiques. En représentant les propositions comme des types et les preuves comme des programmes dans ce langage, nous concevons des traductions de différents systèmes qui sont efficaces et qui préservent leur sens. Ces traductions peuvent ensuite être utilisées pour la vérification indépendante de preuves et l'interopérabilité de preuves. Dans ce travail, nous nous intéressons à la traduction de logiques basées sur la théorie des types qui permettent à la fois le calcul et la quantification d'ordre supérieur comme étapes de raisonnement. Les systèmes de types purs sont un exemple notoire de tels systèmes calculatoires d'ordre supérieur, et forment la base de plusieurs assistants de preuve modernes. Nous concevons une traduction des systèmes de types purs en lambda-Pi calcul modulo réécriture basée sur les travaux de Cousineau et Dowek. La traduction préserve le typage et en particulier préserve donc aussi l'évaluation et le calcul. Nous montrons que la traduction est adéquate en prouvant qu'elle est conservative par rapport au système original. Nous adaptons également la traduction pour inclure la cumulativité d'univers, qui est une caractéristique présente dans les systèmes modernes comme la théorie des types intuitionniste et le calcul des constructions inductives. Nous proposons d'utiliser des coercitions explicites pour traiter le sous-typage implicite présent dans la cumulativité, réconciliant ainsi les systèmes de types purs et la théorie des types avec univers à la Tarski. Nous montrons comment préserver l'expressivité des systèmes d'origine en ajoutant des équations pour garantir que les types ont une représentation unique en tant que termes, conservant ainsi la complétude de la traduction. Les résultats de cette thèse ont été appliqués dans des outils de traduction automatique de preuve. Nous avons implémenté des programmes qui traduisent automatiquement les preuves de HOL, Coq, et Matita, en Dedukti, un vérificateur de types pour le lambda-Pi-calcul modulo réécriture. Ces preuves peuvent ensuite être revérifiées et combinées ensemble pour former de nouvelles théories dans Dedukti, qui joue ainsi le rôle de vérificateur de preuves indépendant et de plateforme pour l'interopérabilité de preuves. Nous avons testé ces outils sur plusieurs bibliothèques. Les résultats expérimentaux confirment que nos traductions sont correctes et qu'elles sont efficaces comparées à l'état des outils actuels.
Type de document :
Thèse
Computer Science [cs]. École polytechnique, 2015. English
Liste complète des métadonnées


https://pastel.archives-ouvertes.fr/tel-01235303
Contributeur : Ali Assaf <>
Soumis le : mercredi 16 décembre 2015 - 01:13:26
Dernière modification le : vendredi 18 décembre 2015 - 01:07:29
Document(s) archivé(s) le : samedi 29 avril 2017 - 15:48:55

Fichier

Identifiants

  • HAL Id : tel-01235303, version 4

Collections

Citation

Ali Assaf. A framework for defining computational higher-order logics. Computer Science [cs]. École polytechnique, 2015. English. <tel-01235303v4>

Partager

Métriques

Consultations de
la notice

488

Téléchargements du document

316