Abstract FR:

Le -calcul est une extension du -calcul associée a la logique classique. Cette thèse contient : - une collection de résultats généraux sur les systèmes de réduction abstraits (lemmes de hindley-rosen, newman et autres) ; - les preuves de la confluence du -calcul avec ou sans la -réduction ; - des résultats de terminaison, de standardisation et de retardement sur les réduction du -calcul ; - une étude sur la forme normale des -termes ; - l'exhibition de -termes operationnellement-equivalents et non calculatoirement-equivalents, avec comme corollaire un contre-exemple au théorème de Böhm ; - une introduction a un -calcul par valeur confluent et qui préserve le type par réduction.