Cette thèse présente un calcul des séquents pour la logique linéaire enrichie d'un connecteur non commutatif et autodual "précède" situé entre le "par" et le "tenseur". Il est défini pour des séquents dont les formules sont orientées par un ordre partiel. Un calcul de réseaux de démonstration quotientant ce calcul des séquents est défini en termes de graphes orientés. Ce calcul est doté d'une sémantique dénotationnelle dans les espaces cohérents, préservée par élimination des coupures, un processus convergent et confluent. Des résultats combinatoires nécessaires sur les ordres partiels et sur la structure des graphes de démonstrations sont établies ainsi que quelques propriétés du calcul commutatif avec la règle MIX.

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérification de démonstrations mathématiques écrites en langue naturelle.<br><br>L'architecture générale du système se décrit en 4 phases :<br>- analyse de la démonstration par des outils linguistiques ;<br>- traduction de la démonstration dans un langage restreint ;<br>- interprétation du texte traduit en un arbre de règles de déduction ;<br>- validation des règles de déduction à l'aide d'un démonstrateur automatique.<br><br>Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens.<br><br>Cette thèse présente plus en détail ce projet et développe principalement les points suivants :<br>- définition du langage restreint et de son interprétation ;<br>- propriétés du type principal de termes d'un lambda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ;<br>- description du démonstrateur automatique.

Ce travail est une contribution à la sémantique de jeux des langages de programmation. Il présente plusieurs méthodes nouvelles pour construire une sémantique de jeux pour un lambda-calcul de continuations.Si les sémantiques de jeux ont été développées à grande échelle pour fournir des modèles de langages fonctionnels avec références, en appel par nom et par valeur, ou pour différents fragments de la logique linéaire, certains de ses aspects demeurent cependant très subtils. Cette thèse s'intéresse spécifiquement à la notion d'innocence et à la combinatoire mise en jeu dans la composition des stratégies innocentes, en donnant pour chacune une interprétation via des constructions catégoriques standards.Nous reformulons la notion d'innocence en terme de préfaisceaux booléens sur une catégorie de vues. Pour cela, nous enrichissons la notion de parties dans notre sémantique de jeux en ajoutant des morphismes entre parties qui vont au-delà du simple ordre préfixe habituel. À partir d'une stratégie, donnée par les vues qu'elle accepte, on calcule son comportement sur toutes les parties en prenant une extension de Kan à droite.La composition des stratégies innocentes s'appuie sur les notions catégoriques habituelles de systèmes de factorisation et de foncteurs polynomiaux. Notre sémantique permet de modéliser l'interaction entre deux stratégies comme une seule stratégie dont il faut parvenir à cacher les coups internes, grâce à une technique d'élimination des coupures~: cette étape est accomplie avec une version affaiblie des systèmes de factorisation. La composition elle-même entre stratégies repose pour sa part sur l'utilisation de la théorie des foncteurs polynomiaux. Les propriétés essentielles, telles que l'associativité ou la correction de la sémantique, proviennent d'une méthode de preuve presque systématique donnée par cette théorie. / This work is a contribution to game semantics for programming languages. We describe new methods used to define a game semantics for a lambda-calculus with continuations.Game semantics have been widely used to provide models for functional programming languages with references, using call-by-name or call-by-value, or for different fragments of linear logic. Yet, some parts of these semantics are still highly subtle. This work mainly deals with the notion of innocence, and with combinatorics involved in composing innocent strategies. We provide both of them with an interpretation which relies on standard categorical constructions.We reformulate innocence in terms of boolean presheaves over a given category of views. We design for this purpose an enriched class of plays, by adding morphisms which do not appear in the traditional preorder of plays. We show how to compute the global behaviour, i.e., on every play, of a strategy given by its class of accepted views by taking a right Kan extension.Our composition of innocent strategies relies on the usual categorial notions of factorisation systems and polynomial functors. In our semantics, the interaction between two strategies is itself a strategy, in which we must hide internal moves with a cut-elimination process. This step is given by a weakened version of factorisations systems. The core of composition of strategies involves material borrowed from polynomial functors theory. This theory yields a systematic proof method for showing essential properties, such as associativity of composition, or correction of our semantics.

La réalisabilité classique de Jean-Louis Krivine associe à chaque modèle de calcul et chaque modèle de la théorie des ensembles un nouveau modèle de la théorie des ensembles, appelé modèle de réalisabilité, d'une façon similaire au forcing. Chaque modèle de réalisabilité est muni d’une algèbre de Boole caractéristique $\gimel 2$ (gimel 2), dont la structure donne des informations sur les propriétés du modèle de réalisabilité. En particulier, les modèles de forcing correspondent au cas où $\gimel 2$ est l'algèbre de Boole à deux éléments.Ce travail présente de nouveaux outils pour manipuler les modèles de réalisabilité et donne de nouveaux résultats obtenus en les exploitant. L'un d'entre eux est qu'au premier ordre, la théorie des algèbres de Boole à au moins deux éléments est complète pour $\gimel 2$, au sens où $\gimel 2$ eut être rendue élémentairement équivalente à n'importe quelle algèbre de Boole. Deux autres résultats montrent que $\gimel 2$ peut être utilisée pour étudier les modèles dénotationnels de langage de programmation (chacun part d'un modèle dénotationnel et classifie ses degrés de parallélisme à l'aide de $\gimel 2$). Un autre résultat montre que la technique de Jean-Louis Krivine pour réaliser l'axiome des choix dépendants à partir de l'instruction quote peut se généraliser à des formes plus fortes de choix. Enfin, un dernier résultat, obtenu en collaboration avec Laura Fontanella, accompagne le précédent en adaptant la condition d'antichaîne dénombrable du forcing au cadre de la réalisabilité, ce qui semble semble ouvrir une piste prometteuse pour réaliser l'axiome du choix. / Jean-Louis Krivine's classical realizability defines, from any given model of computation and any given model of set theory, a new model of set theory called the realizability model, in a similar way to forcing. Each realizability model is equipped with a characteristic Boolean algebra $\gimel 2$ (gimel 2), whose structure encodes important information about the properties of the realizability model. For instance, forcing models are precisely the realizability models in which $\gimel 2$ is the Boolean algebra with to elements.This document defines new tools for studying realizability models and exploits them to derive new results. One such result is that, as far as first-order logic is concerned, the theory of Boolean algebras with at least two elements is complete for $\gimel 2$, meaning that for each Boolean algebra B (with at least two elements), there exists a realizability model in which $\gimel 2$ is elementarily equivalent to B. Next, two results show that $\gimel 2$ can be used as a tool to study denotational models of programming languages (each one of them takes a particular denotational model and classifies its degrees of parallelism using $\gimel 2$). Moving to set theory, another results generalizes Jean-Louis Krivine's technique of realizing the axiom of dependant choices using the instruction quote to higher forms of choice. Finally, a last result, which is joint work with Laura Fontanella, complements the previous one by adapting the countable antichain condition from forcing to classical realizability, which seems to open a new, promising approach to the problem of realizing the full axiom of choice.

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.

Le thème général de cette thèse est l’exploitation de l’interaction entre la sémantique dénotationnelle et la syntaxe. Des sémantiques satisfaisantes ont été découvertes pour les preuves en logique intuitionniste et linéaire, mais dans le cas de la logique classique, la solution du problème est connue pour être particulièrement difficile. Ce travail commence par l’étude d’une interprétation concrète des preuves classiques dans la catégorie des ensembles ordonnés et bimodules, qui mène à l’extraction d’invariants significatifs. Suit une généralisation de cette sémantique concrète, soit l’interprétation des preuves classiques dans une catégorie compacte fermée où chaque objet est doté d’une structure d’algèbre de Frobenius. Ceci nous mène à une définition de réseaux de démonstrations pour la logique classique. Le concept de correction, l’élimination des coupures et le problème de la “full completeness” sont abordés au moyen d’un enrichissement naturel dans les ordres sur la catégorie de Frobenius, produisant une catégorie pour l'élimination des coupures et un concept de ressources pour la logique classique. Revenant sur notre première sémantique concrète, nous montrons que nous avons une représentation fidèle de la catégorie de Frobenius dans la catégorie des ensembles ordonnés et bimodules. / The general theme of this thesis is the exploitation of the fruitful interaction between denotational semantics and syntax. Satisfying semantics have been discovered for proofs in intuitionistic and certain linear logics, but for the classical case, solving the problem is notoriously difficult.This work begins with investigations of concrete interpretations of classical proofs in the category of posets and bimodules, resulting in the definition of meaningful invariants of proofs. Then, generalizing this concrete semantics, classical proofs are interpreted in a free symmetric compact closed category where each object is endowed with the structure of a Frobenius algebra. The generalization paves a way for a theory of proof nets for classical proofs. Correctness, cut elimination and the issue of full completeness are addressed through natural order enrichments defined on the Frobenius category, yielding a category with cut elimination and a concept of resources in classical logic. Revisiting our initial concrete semantics, we show we have a faithful representation of the Frobenius category in the category of posets and bimodules.

Cette thèse, s'intéresse aux systèmes d'interaction, une notion visant à modéliser les interactions entre un système informatique et son environnement.<br /><br />La première partie développe, dans le cadre de la théorie des types de Martin-Löf, la théorie de base des systèmes d'interaction et des constructions inductives et co-inductives qu'ils permettent. On trouve dans cette partie une étude des liens entre systèmes d'interaction et topologies formelles et une formulation (en terme de systèmes d'interaction) d'un théorème de complétude vis-à-vis d'une sémantique topologique des théories géométriques (linéaires).<br /><br />Dans cette étude, la notion complètement standard de simulation, joue un rôle fondamental car elle permet de définir la notion de morphisme entre systèmes d'interaction. Ceci permet d'établir une équivalence entre la catégorie ainsi définie et une autre catégorie, beaucoup plus simple à décrire, celle des transformateurs de prédicats.<br /><br />En traduisant dans ce nouveau vocabulaire les constructions précédentes, on observe que les transformateurs de prédicats forment un nouveau modèle de la logique linéaire, qui est décrit puis étendu au second ordre.<br /><br />Enfin, les propriétés particulières des systèmes d'interaction / transformateurs de prédicats sont mises à profit pour donner une interprétation du lambda-calcul différentiel. Cela suppose d'introduire du non déterminisme, ce que les systèmes d'interaction et les transformateurs de prédicats permettent de faire.

Cette thèse, s'intéresse aux systèmes d'interaction, une notion visant à modéliser les interactions entre un système informatique et son environnement.<br /><br />La première partie développe, dans le cadre de la théorie des types de Martin-Löf, la théorie de base des systèmes d'interaction et des constructions inductives et co-inductives qu'ils permettent. On trouve dans cette partie une étude des liens entre systèmes d'interaction et topologies formelles et une formulation (en terme de systèmes d'interaction) d'un théorème de complétude vis-à-vis d'une sémantique topologique des théories géométriques (linéaires).<br /><br />Dans cette étude, la notion complètement standard de simulation, joue un rôle fondamental car elle permet de définir la notion de morphisme entre systèmes d'interaction. Ceci permet d'établir une équivalence entre la catégorie ainsi définie et une autre catégorie, beaucoup plus simple à décrire, celle des transformateurs de prédicats.<br /><br />En traduisant dans ce nouveau vocabulaire les constructions précédentes, on observe que les transformateurs de prédicats forment un nouveau modèle de la logique linéaire, qui est décrit puis étendu au second ordre.<br /><br />Enfin, les propriétés particulières des systèmes d'interaction / transformateurs de prédicats sont mises à profit pour donner une interprétation du lambda-calcul différentiel. Cela suppose d'introduire du non déterminisme, ce que les systèmes d'interaction et les transformateurs de prédicats permettent de faire.