Dans les années quatre-vingts-dix, on a remarqué ce que l'isomorphisme de Curry-Howard peut être étendu à la logique classique. De nombreux calculs ont été développés pour constituer la base de cette extension. On étudie dans cette thèse quelques uns de ces calculs.<br />On étudie tout d'abord le $\lambda \mu$-calcul simplement typé de Parigot. Parigot a prouvé par des méthodes sémantiques que son calcul est fortement normalisable. Ensuite, David et Nour ont donné une preuve arithmétique de la normalisation forte de ce calcul avec la règle $\mu'$ (règle duale de $\mu$). Cependant, si l'on ajoute au $\lambda \mu \mu'$-calcul la règle de simplification $\rho$, la normalisation forte est perdu. On montre que le $\mu \mu' \rho$-calcul non-typé est faiblement normalisable, et que le $\lambda \mu \mu' \rho$-calcul typé est aussi faiblement normalisable. De plus, on examine les effets d'ajouter quelques autre règles de simplification.<br />On établi ensuite une borne de la longueur des séquences de réduction en $\lambda \mu \rho \theta$-calcul simplement typé.<br />Ce résultat est une extension de celui de Xi pour le $\lambda$-calcul simplement typé.<br />Dans le chapitre suivant on présente une preuve arithmétique de la normalisation forte du $\lambda$-calcul symétrique de Berardi et Barbanera.<br />Enfin, on établi des traductions entre le $\lambda$-calcul symétrique de Berardi et Barbanera et le $\lmts$-calcul, qui est le $\lmt$-calcul de Curien et Herbelin étendu avec une négation. (... qui est obtenu du $\lmt$-calcul de Curien et Herbelin par l'étendre avec une négation).

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.<br>Les principaux résultats de cette thèse sont :<br>- La standardisation, la confluence et une extension de la machin de J.-L. Krivine en $\lambda \mu^{\wedge \vee}$-calcul.<br>- Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures.<br>- 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.<br>- Un théorème de complétude pour le $\lambda \mu$-calcul simplement typé.<br>- Une introduction à un $\lambda \mu^{\wedge \vee}$-calcul par valeur confluent.

Cette thèse de théorie de la démonstration étudie les interactions entre le λ-calcul différentiel d'Ehrhard et Regnier d'un côté, et certaines émanations calculatoires de la logique classique (le λμ-calcul de Parigot et le λ-barre-μ-calcul de Herbelin) de l'autre. L'étude est initiée et guidée par la décomposition de ces calculs dans des extensions de la logique linéaire de Girard.<br /><br />Dans une première partie, on définit un cadre commun pour ces extensions, dans le formalisme des réseaux d'interaction de Lafont, et on y rappelle des résultats de la littérature ou du folklore. On donne en particulier la traduction du λμ-calcul et du λ-barre-μ-calcul dans les réseaux polarisés de Laurent et celle du fragment finitaire du λ-calcul différentiel dans les réseaux différentiels d'Ehrhard et Regnier.<br /><br />Dans la deuxième partie, on introduit les réseaux différentiels polarisés (RDP), comme l'extension par une polarisation à la Laurent des réseaux différentiels. La pertinence des règles de réduction nouvelles est soulignée par l'étude d'un modèle dénotationnel commun aux réseaux différentiels et aux réseaux polarisés.<br /><br />Enfin, on présente trois calculs de termes, chacun pouvant être considéré comme une lecture en arrière de tout ou partie des interactions définies par les RDP : un λμ-calcul différentiel, qui correspond à la réunion des réseaux différentiels et des réseaux polarisés ; un λ-barre-μ-calcul avec produit de convolution sur les piles, qui fait intervenir la structure de bigèbre des types polarisés introduite dans les RDP, mais pas la dérivée ; enfin, un λ-barre-μ-calcul différentiel qui développe toute l'expressivité des RDP.

Les travaux de cette thèse se situent dans le cadre de la linguistique computationnelle. La problématique est de définir une interface syntaxe / sémantique basée sur les théories de la grammaire générative.<br />Une première partie, concernant le problème de l'analyse syntaxique, présente tout d'abord, la syntaxe générative, puis un formalisme la réalisant: les grammaires minimalistes de Stabler. <br />À partir de ces grammaires, nous réalisons une étude sur les propriétés de l'opération de fusion pour laquelle nous définissons des notions d'équivalence, ainsi qu'une modélisation abstraite des lexiques.<br />Une seconde partie revient sur le problème de l'interface. Pour cela, nous proposons un formalisme de type logique, basé sur la logique mixte (possédant des connecteurs commutatifs et non-commutatifs), qui équivaut, sous certaines conditions, aux grammaires de Stabler. <br />Dans ce but, nous introduisons une normalisation des preuves de cette logique, normalisation permettant de vérifier la propriété de la sous-formule. Ces propriétés sont également étendues au calcul de Lambek avec produit.<br />À partir de l'isomorphisme de Curry-Howard, nous synchronisons un calcul sémantique avec les preuves réalisant l'analyse syntaxique. Les termes de notre calcul font appel aux propriétés du lambda mu-calcul, ainsi qu'à celles de la DRT (Discourse Representative Theory).<br />Une dernière partie applique ces formalismes à des cas concrets. Nous établissons des fragments d'une grammaire du français autour du problème des clitiques.

Cette thèse étudie deux modèles de réalisabilité pour la logique classique construits sur la sémantique des jeux HO, interprétant la logique, l'arithmétique et l'analyse classiques directement par des programmes manipulant un espace de stockage d'ordre supérieur.La non-innocence en jeux HO autorise les références d'ordre supérieur, et le non parenthésage révèle la CPS des jeux HO et fournit une catégorie de continuations dans laquelle interpréter le lambda-mu calcul de Parigot. Deux modèles de réalisabilité sont construits sur cette interprétation calculatoire directe des preuves classiques.Le premier repose sur l'orthogonalité, comme celui de Krivine, mais il est simplement typé et au premier ordre. En l'absence de codage de l'absurdité au second ordre, une mu-variable libre dans les réaliseurs permet l'extraction. Nous définissons un bar-récurseur et prouvons qu'il réalise l'axiome du choix dépendant, utilisant deux conséquences de la structure de CPO du modèle de jeux: toute fonction sur les entiers (même non calculable) existe dans le modèle, et toute fonctionnelle sur des séquences est Scott-continue. La bar-récursion est habituellement utilisée pour réaliser intuitionnistiquement le « double negation shift » et en déduire la traduction négative de l'axiome du choix. Ici, nous réalisons directement l'axiome du choix dans un cadre classique.Le second, très spécifique au modèle de jeux, repose sur des conditions de gain: des ensembles de positions d'un jeu munis de propriétés de cohérence. Un réaliseur est alors une stratégie dont les positions sont toutes gagnantes. / This thesis investigates two realizability models for classical logic built on HO game semantics. The main motivation is to have a direct computational interpretation of classical logic, arithmetic and analysis with programs manipulating a higher-order store.Relaxing the innocence condition in HO games provides higher-order references, and dropping the well-bracketing of strategies reveals the CPS of HO games and gives a category of continuations in which we can interpret Parigot's lambda-mu calculus. This permits a direct computational interpretation of classical proofs from which we build two realizability models.The first model is orthogonality-based, as the one of Krivine. However, it is simply-typed and first-order. This means that we do not use a second-order coding of falsity, and extraction is handled by considering realizers with a free mu-variable. We provide a bar-recursor in this model and prove that it realizes the axiom of dependent choice, relying on two consequences of the CPO structure of the games model: every function on natural numbers (possibly non computable) exists in the model, and every functional on sequences is Scott-continuous. Usually, bar-recursion is used to intuitionistically realize the double negation shift and consequently the negative translation of the axiom of choice. Here, we directly realize the axiom of choice in a classical setting.The second model relies on winning conditions and is very specific to the games model. A winning condition is a set of positions in a game which satisfies some coherence properties, and a realizer of a formula is then a strategy which positions are all winning.

Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.