Generic Proof Tools and Finite Group Theory

Résumé : Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.
Type de document :
Thèse
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2011. English


https://pastel.archives-ouvertes.fr/pastel-00649586
Contributeur : François Garillot <>
Soumis le : jeudi 12 janvier 2012 - 11:18:47
Dernière modification le : mardi 28 juillet 2015 - 12:58:17
Document(s) archivé(s) le : lundi 19 novembre 2012 - 13:20:09

Identifiants

  • HAL Id : pastel-00649586, version 1

Collections

Citation

François Garillot. Generic Proof Tools and Finite Group Theory. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2011. English. <pastel-00649586>

Exporter

Partager

Métriques

Consultations de
la notice

557

Téléchargements du document

558