Résumé: L'objet de cette thèse est l’étude des systèmes formels du type des systèmes lj et lk de gentzen (couramment appeles calculs des sequents) dans leur rapport avec la calculabilité. Le procédé de calcul dans ces systèmes consiste en l’élimination des coupures. Deux interprétations sont considérées. Le lambda-calcul constitue le support de la première interprétation. Nous établissons une correspondance de type curry-howard entre lj et une variante syntaxique du lambda-calcul avec opérateur explicite de substitution (de type let - in - ). Une procédure de normalisation/élimination des coupures confluente et terminant fortement est donnée et l'extension de la correspondance a lk se fait en considérant l’opérateur mu du lambda-mu-calcul de parigot. La théorie des jeux constitue le support de la deuxième interprétation : les preuves des calculs des sequents sont vues comme des stratégies gagnantes pour certains types de jeux a deux joueurs (dialogues) se disputant la validité de la formule prouvée. Nous donnons deux résultats. Dans un premier temps, nous montrons qu'il suffit de considérer des restrictions ljq de lj puis lkq de lk pour établir, dans le cas propositionnel, une bijection entre les preuves de ces systèmes et les e-dialogues intuitionnistes puis classiques définis par lorenzen dans un but de fondement de la prouvabilite en termes de jeux. Ceci affine et generalise un résultat de felscher d’équivalence entre l'existence d'une preuve d'une formule a dans lj et l'existence d'une stratégie gagnante pour le premier des joueurs dans un e-dialogue a propos de a. Dans un deuxième temps, nous partons d'une logique propositionnelle infinitaire sans variable considérée par coquand pour y définir une interaction prouvée terminante entre les preuves vues comme stratégies gagnantes. Nous montrons une correspondance opérationnelle entre ce procédé d'interaction et l’élimination faible de tête des coupures, celle-ci étant indépendamment prouvée terminante.

Paris:
Langue: Français
Collation: 127 p. ill. ;30 cm.
Diplôme: Doctorat
Etablissement de soutenance: Paris, Université Pierre et Marie Curie. Institut Blaise Pascal
Spécialité: Informatique
Index décimal 621 .Physique appliquée (électrotechnique, génie civil, génie mécanique, ingénierie appliquée, principes physiques en ingénierie)
Thème Informatique

Mots clés:
Lambda-calcul
Sciences appliquées :Informatique
Logique propositionnelle

Note: Bibliogr. pp.121-123