[tel-00415845, v1] Etude d'un $ lambda$-calcul issu d'une logique classique

1Universit´e de SavoieU.F.R. Sciences Fondamentales et Appliqu´eesLaboratoire de Math´ematiques LAMATh`esepour obtenir le grade deDocteur de l’Universit´e de SavoieDiscipline : Math´ematiquesTitre :´Etude d’un λ-calcul issu d’unelogique classiquepr´esent´ee et soutenue parKhelifa SABERLe 6 juillet 2007dirig´ee parKarim NOURJury compos´e de:Ph. De Groote RapporteurR. Matthes RappR. David ExaminateurT. Ehrhard ExaminateurH. HerbelinteurK. Nour Directeurtel-00415845, version 1 - 11 Sep 20092tel-00415845, version 1 - 11 Sep 20093”Nous ´elevons en rang qui Nous voulons et au-dessus detout savant se trouve un savantissime.”Coran 12, 76.tel-00415845, version 1 - 11 Sep 20094tel-00415845, version 1 - 11 Sep 20095D´edicaces`A celle qui a toujours compt´e pour moi et qui compteraaussi longtemps que je vivrai, Ma M`ere.`A Mon P`ere, symbole de patience et de r´esistance.`A ma femme, mes fr`eres et soeurs, vous ˆetes le sourirede ma vie.tel-00415845, version 1 - 11 Sep 20096tel-00415845, version 1 - 11 Sep 20097RemerciementsSe lancer dans l’aventure d’une th`ese, c’´etait difficile mais il a ´et´e encore plusdifficile de la mener a` terme. On s’inqui`ete, on doute et surtout on souffre. Lestress, les incertitudes... on frˆole la d´epression. Mais quand on a un directeurqui s’appelleKarim, on s’accroche et on y croit. Je tiens `a lui adresser mes pro-fonds remerciements, sans son encadrement bienveillant, ses conseils et ses id´ees,ce ...