Etude d'un $\lambda$-calcul issu d'une logique classique

The $\lambda \mu^{\wedge \vee}$-calculus is an extension of the $\lambda$-calculus associated to the full classical natural deduction.The main results of this thesis are:- A standardization theorem, the confluence theorem, and an extension of J.-L. Krivine machine to the $\lambda \mu^{\wedge \vee}$-calculus.- A semantical proof of the strong normalization theorem of the cut elimination procedure. - A semantics of realizability for the $\lambda \mu^{\wedge \vee}$-calculus and characterization of the operational behavior of some closed typed terms.- A completeness theorem for the simply typed $\lambda \mu$-calculus.- A confluent call-by-value $\lambda \mu^{\wedge \vee}$-calculus.Le $\lambda \mu^{\wedge \vee}$-calcul est une extension du $\lambda$-calcul associée à la déduction naturelle classique où sont considérés tous les connecteurs.Les principaux résultats de cette thèse sont :- La standardisation, la confluence et une extension de la machin de J.-L. Krivine en $\lambda \mu^{\wedge \vee}$-calcul.- Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures.- Une sémantique de réalisabilité pour le $\lambda \mu^{\wedge \vee}$-calcul qui permet de caractériser le comportement calculatoire de certains termes typés et clos.- Un théorème de complétude pour le $\lambda \mu$-calcul simplement typé.- Une introduction à un $\lambda \mu^{\wedge \vee}$-calcul par valeur confluent