Return to search

Typage et déduction dans le calcul de réécriture

Le calcul de réécriture est un lambda-calcul avec filtrage. Cette thèse est consacrée à l'étude de systèmes de types pour ce calcul et à son utilisation dans le domaine de la déduction.<br /><br />Nous étudions deux paradigmes de typage. Le premier est inspiré du lambda-calcul simplement typé, mais un terme peut y être typé sans être terminant. Nous l'utilisons donc pour représenter des programmes et des systèmes de réécriture. La seconde famille de systèmes de types que nous étudions est adaptée des Pure Type Systems. Nous en démontrons la normalisation forte grâce à une traduction vers le lambda-calcul typé.<br /><br />Enfin nous proposons deux approches pour l'utilisation du calcul de réécriture en logique. La première consiste à définir des termes de preuve pour la déduction modulo à l'aide des systèmes fortement normalisants. Dans la seconde, nous définissons une généralisation de la déduction naturelle et nous montrons que le filtrage est utile pour représenter les règles de ce système de déduction.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00010546
Date07 October 2005
CreatorsWack, Benjamin
PublisherUniversité Henri Poincaré - Nancy I
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0021 seconds