Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00134646 |
| Date | 08 December 2006 |
| Creators | Lengrand, Stéphane |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0032 seconds