La ludique, introduite par Jean-Yves Girard, est un modèle de la logique linéaire sans exponentielles. En vue de la modélisation des exponentielles, cette thèse propose deux extensions successives de la ludique. La première extension étend la ludique en un modèle probabiliste original conservant la plupart des théorèmes du modèle initial. La seconde extension reprend ce modèle probabiliste et utilise des pointeurs, introduits dans les jeux de Hyland et Ong, ce qui permet de considérer les répétitions et donc de modéliser les exponentielles.<br /><br />Un résultat de complétude est montré pour la ludique probabiliste vis-à-vis de la ludique et de la logique MALL2. La ludique exponentielle proposée vérifie les théorèmes principaux de la ludique : les théorèmes analytiques. En particulier, ce modèle montre une interprétation de la logique linéaire avec des répétitions gardant une topologie séparée. De plus, les coefficients introduits apporte à la ludique une "plus grande séparation" que dans le modèle d'origine.

Les sémantiques de jeux s'attachent à caractériser le comportement interactif des preuves et des programmes, en les modélisant par des stratégies qui décrivent la façon dont ils réagissent à leur environnement. Afin de prendre en compte les aspects concurrents des preuves en logique linéaire, nous avons été amenés à retravailler les notions et techniques classiques de sémantique des jeux pour les étendre à un cadre asynchrone et non-alterné. Dans une première partie, nous définissons une famille de stratégies asynchrones donnant lieu à un modèle de logique linéaire, pleinement complet pour le fragment multiplicatif. Ces stratégies sont définies de façon locale par une série d'axiomes diagrammatiques ; elles sont ensuite raffinées par un critère dynamique d'ordonnancement, dont nous montrons qu'il impose une version orientée du critère de correction des réseaux de preuve. Cette formulation asynchrone permet d'unifier des modèles variés de la logique linéaire - aussi bien séquentiels que concurrents, dynamiques que statiques - où les preuves sont vues comme des stratégies séquentielles, des stratégies concurrentes, des relations ou des structures d'événements. Dans une seconde partie, nous abordons une autre approche pour décrire la causalité induite par les preuves et introduisons une sémantique de jeux capturant les dépendances engendrées par les connecteurs du premier ordre en logique propositionnelle. Nous montrons que la catégorie résultante peut être finiment présentée par un 2-polygraphe et étudions la possibilité d'orienter cette présentation en un système de réécriture confluent, notamment en introduisant un algorithme d'unification dans ce cadre 2-dimensionnel.

Cette thèse s'articule autour de l'utilisation de stratégies totales pour la représentation des preuves. La première partie porte sur le cadre finitaire. L'analyse commence dans un univers syntaxique : on définit un lambda-calcul unaire fortement normalisant, pour lequel on rappelle la machine à pointeurs (PAM). On réduit le problème de préservation de la totalité par composition à un problème de finitude sur des objets appelés structures de pointeurs. On donne trois preuves différentes de ce résultat de finitude. La première se ramène via la PAM à la normalisation du lambda-calcul unaire, la seconde passe par l'extraction d'une réduction simple sur les arbres d'entiers et la troisième s'inspire d'un argument combinatoire de Coquand. La seconde partie traite d'un calcul de séquents mu-LJ équipé de définitions inductives et coinductives, dans lequel on donne une simulation du système T. On définit les catégories mu-fermées, formant une classe de modèles de mu-LJ. Dans le cadre des jeux on définit les arènes ouvertes, munies de variables de type libres. À chacune de ces arènes ouvertes est associé un foncteur ouvert sur la catégorie des stratégies innocentes. On décrit ensuite sur les arènes ouvertes une construction de boucle dont on montre qu'elle rejoint le modèle de McCusker des types récursifs. Les boucles sont alors enrichies par des conditions de gain inspirées des jeux de parité, ce qui équipe les foncteurs ouverts d'algèbres initiales et coalgèbres terminales et construit une catégorie mu-fermée. On propose finalement une extension de mu-LJ à une syntaxe infinie, pour laquelle le modèle est pleinement complet.

Issue des travaux sur la logique linéaire et l'analyse calculatoire de la logique classique, la notion de polarités semble jouer un rôle essentiel dans l'étude actuelle des systèmes logiques. La polarisation est une contrainte qui simplifie les objets tout en conservant une expressivité suffisante d'un point de vue informatique.<br /><br />L'objet de cette thèse est d'étudier et d'exploiter cette nouvelle structure afin en particulier de mettre à jour les relations entre la logique classique et la logique linéaire (LL). L'introduction des polarités dans LL permet de mieux appréhender ce vaste système et de prolonger le développement de différents outils trop complexes en l'absence de cette contrainte. Nous définissons ainsi, pour la logique linéaire polarisée (LLP), des réseaux de preuve intégrant les connecteurs additifs de manière satisfaisante, une sémantique des jeux polarisés qui réconcilie jeux et dualité, une géométrie de l'interaction parallèle et d'autres sémantiques dénotationnelles basées sur des notions connues (espaces de corrélation, catégories de contrôle).<br /><br />Il est important de montrer que malgré cette contrainte, LLP reste un système suffisamment expressif. Pour cela nous étudions en détail les traductions des différents systèmes de logique classique déterministe connus (LC, lambda-mu calcul, ...) aussi bien en appel par nom qu'en appel par valeur. De surcroît, les traductions obtenues pour ces systèmes sont plus simples que celles vers LL.<br /><br />Enfin la souplesse de ces traductions nous permet d'analyser plus finement certaines propriétés de la logique classique tout comme LL permet d'analyser la logique intuitionniste. On peut ainsi étudier un équivalent linéaire des CPS-traductions.

La sémantique des jeux permet l'étude et la modélisation abstraite des langages de programmation d'un point de vue mathématique, en gardant assez d'informations concrètes sur la structure des programmes, mais en laissant de côté les détails superflus. Durant mon doctorat, j'ai travaillé sur l'association de la sémantique des jeux avec les structures d'événements pour proposer des modèles dénotationnels vraiment concurrents de langages concurrents d'ordresupérieur. Dans un premier temps, je construis un modèle réalisant cette association, qui retient suffisamment d'informations sur le comportement des programmes pour interpréter adéquatement une grande variété de langages concurrents et non déterministes pour des notions fines de convergences. La construction de ce modèle se base surl'introduction de symétrie afin d'établir que le modèle forme une catégorie cartésienne fermée. Dans un second temps, je propose une généralisation dans ce cadre des notions d'innocence et de bon parenthésage, essentielles en sémantiquedes jeux pour comprendre les effets calculatoires, et résolvant ainsi des problèmes ouverts de la sémantique des jeux concernant l'innocence concurrente et non-déterministe. Dans un dernier temps je propose une interprétation dans ce modèle, de langages concurrents avec mémoire faible, un des premiers travaux de sémantique dénotationnelle pour ce type de langages. Bien que théoriques, ces modèles sont compositionnels et basés sur des ordres partiels, et donc pourraient permettre de faire passer la vérification de programmes concurrents à l'échelle (une problématique importante du domaine). / Game semantics is an effective tool to study and model abstractly programming languages from a mathematical point of view, by keeping enough concrete information on the structure of programs but yet leaving aside superfluous details. During my PhD thesis, I worked on merging game semantics with event structures to propose truly concurrent denotational models of higher-order concurrent languages. In the first part, I build a model based on this merge, retaining enough information about the behaviour of programs to interpret adequately a large variety of concurrent programming languages for various notions of convergence. The construction of this model is based on the introduction of symmetry to prove that the model is indeed in a cartesian-closed category. In the second part, I propose a generalization, in this setting, of innocence and well-bracketing, key notions in game semantics to understand the computational effects, and thusly closing openproblems of game semantics about concurrent and nondeterministic innocence.In the last part, I propose an interpretation in this model of concurrent languages with weak shared memory, one of the first works of denotational semantics for these kinds of languages. Althoughtheoretical, these models are compositional and based on partial orders, and thus could permit scaling verification of concurrent programs (an important problem of the domain).

Prouver l’équivalence de programmes écrits dans un langage fonctionnel avec références est un problème notoirement difficile. L’objectif de cette thèse est de proposer un système logique dans lequel de telles preuves peuvent être formalisées, et dans certains cas inférées automatiquement. Dans la première partie, une méthode générique d’extension de la théorie des types dépendants est proposée, basée sur une interprétation du forcing vu comme une traduction de préfaisceaux de la théorie des types. Cette extension dote la théorie des types de constructions récursives gardées, qui sont utilisées ensuite pour raisonner sur les références d’ordre supérieure. Dans une deuxième partie, nous définissons une sémantique des jeux nominale opérationnelle pour un langage avec références d’ordre supérieur. Elle marie la structure catégorique de la sémantique des jeux avec une représentation sous forme de traces de la dénotation des programmes, qui se calcule de manière opérationnelle et dispose donc de bonnes propriétés de modularité. Cette sémantique nous permet ensuite de prouver la complétude de relations logiques à la Kripke définit de manière directe, via l’utilisation de types récursifs gardés, sans utilisation de la biorthogonalité. Une telle définition directe nécessite l’utilisation de mondes omniscient et un contrôle fin des locations divulguées. Finalement, nous introduisons une logique temporelle qui donne un cadre pour définir ces relations logiques à la Kripke. Nous ramenons alors le problème de l’équivalence contextuelle à la satisfiabilité d’une formule de cette logique générée automatique, c’est à dire à l’existence d’un monde validant cette formule. Sous certaines conditions, cette satisfiabilité peut être décidée via l’utilisation d’un solveur SMT. La complétude de notre méthode devrait permettre d’obtenir des résultats de décidabilité pour l’équivalence contextuelle de certains fragment du langage considéré, en fournissant un algorithme pour construire de tels mondes. / Proving program equivalence for a functional language with references is a notoriously difficult problem. The goal of this thesis is to propose a logical system in which such proofs can be formalized, and in some cases inferred automatically. In the first part, a generic extension method of dependent type theory is proposed, based on a forcing interpretation seen as a presheaf translation of type theory. This extension equips type theory with guarded recursive constructions, which are subsequently used to reason on higher-order references. In the second part, we define a nominal game semantics for a language with higher-order references. It marries the categorical structure of game semantics with a trace representation of denotations of programs, which can be computed operationally and thus have good modularity properties. Using this semantics, we can prove the completeness of Kripke logical relations defined in a direct way, using guarded recursive types, without using biorthogonality. Such a direct definition requires omniscient worlds and a fine control of disclosed locations. Finally, we introduce a temporal logic which gives a framework to define these Kripke logical relations. The problem of contextual equivalence is then reduced to the satisfiability of an automatically generated formula defined in this logic, i.e. to the existence of a world validating this formula. Under some conditions, this satisfiability can be decided using a SMT solver. Completeness of our methods opens the possibility of getting decidability results of contextual equivalence for some fragments of the language, by giving an algorithm to build such worlds.

Cette thèse présente la logique tensorielle, une version primitive de la logique linéaire où la négation involutive est remplacée par une négation tensorielle. Pour illustrer ce point de vue, nous reformulons les espaces cohérents et les espaces de finitude comme deux modèles de logique linéaire obtenus à partir d'un même modèle de logique tensorielle dont on fait varier la négation. La sémantique de la logique tensorielle est pour nous avant tout catégorique, construite autour des notions de catégorie de dialogue et de modalité de ressource. Nous en donnons un modèle inspiré des jeux de Conway où tous les connecteurs, en particulier les modalités de ressource, sont interprétées de manière non dégénérée. Afin de construire ces modalités de ressource de façon plus automatique, nous développons un cadre pour le calcul des algèbres libres d'une T-théorie enrichie. Cette construction, basée sur la notion d'équipement en distributeurs, repose sur deux propriétés : l'une de nature combinatoire, l'opéradicité; l'autre de nature algébrique, la complétude algébrique. Nous présentons ensuite un modèle de jeux équipé d'une trace et d'une notion de multiparenthésage. Le contrôle obtenu par le multiparenthésage est alors vu comme une gestion des ressources. Nous utilisons ce modèle pour interpréter une langage avec références d'ordre supérieur. Nous nous tournons enfin vers des sémantiques de plus bas niveau. Dans un premier temps, nous étudions la structure multicatégorique induite par une catégorie de dialogue. Cela nous amène à définir les multicatégories de contrôle. Dans un second temps, nous formalisons en Coq une propriété de sûreté par le typage d'un compilateur vers un langage assembleur. Cette formalisation repose sur la définition d'une sémantique relationnelle des états de la mémoire dont la structure est inspirée des catégories de dialogue.

La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.

Cette thèse s’intéresse à la sémantique dénotationnelle (en théorie desmodèles et en théorie des jeux) de quatre langages de programmation logique: - LP, le plus restrictif de tous, - DLP, une extension de LP aux disjonctions, - LPN, une extension de LP aux négations, et - DLPN, qui inclut les deux.Ce manuscrit apporte trois contributions principales:(1) Un cadre abstrait pour la sémantique de la programmation logique yest défini, et toutes les approches sémantiques que nous étudions par lasuite prennent place dans ce cadre.Nous définissons la notion générale d'espace de valeurs de vérité commeune structure algébrique spécifique, satisfaisant un certain ensembled'axiomes. Les booléens forment l'exemple canonique d'un tel espace,mais nous devons étudier des cas plus généraux si nous voulonsconsidérer la "négation par l'échec". Pour cela, nous définissons etétudions une famille infinie d'espaces, paramétrée par un ordinal.(2) Une sémantique des jeux pour LP a été définie en 1986, et son étudea été approfondie en 1998. Elle a ensuite été étendue au cas desprogrammes LPN en 2005.Ici nous développons en détails une sémantique pour les programmes DLP.Nous prouvons qu'elle est correcte et complète par rapport aux modèlesminimaux de Minker.(3) Nous définissons un opérateur sémantique qui, étant donnée une sémantique abstraite d'un langage non disjonctif, la transforme en une sémantique disjonctive associée.La correction de cette transformation découle du fait qu'elle conserveles équivalences de sémantiques.Nous en présentons ensuite quelques applications qui permettent, entre autres, d'obtenir la première sémantique des jeux pour DLPN. / In this thesis, we study denotational semantics (model-theoretic andgame-theoretic) of four logic programming languages:- LP which is the most restrictive one;- DLP which extends LP by allowing disjunctions;- LPN which extends LP by allowing negations; and- DLPN which allows both.The three main contributions of this dissertation can be summarized as follows:(1) An abstract framework for logic programming semantics is definedand all semantic approaches that we study are placed within this framework.We define the general notion of a truth value space as an appropriate algebraicstructure that satisfies a set of axioms.The booleans form the canonical example of such a space, but we need toconsider much more general ones when dealing with negation-as-failure. Forthis we define and study an infinite family of spaces, parametrized over anordinal number.(2) A game semantics for LP was defined in 1986 and further studied in 1998.Then in 2005 it was extended for the case of LPN programs.Here a game semantics for DLP programs is developed in full detail; we provethat it is sound and complete with respect to the standard, minimal modelssemantics of Minker.(3) We define a semantic operator which transforms any given abstractsemantics of a non-disjunctive language to a semantics of the"corresponding" disjunctive one. We exhibit the correctness of thistransformation by proving that it preserves equivalences of semantics,and we present some applications of it, obtaining new game semantics forDLPN, among others.

Les grammaires catégorielles abstraites (ou λ-grammaires) sont un formalisme basé sur le λ-calcul simplement typé. Elles peuvent être vues comme des grammaires générant de tels termes, et ont été introduites afin de modéliser l’interface entre la syntaxe et la sémantique du langage naturel, réunissant deux idées fondamentales : la distinction entre tectogrammaire (c.a.d. structure profonde d’un énoncé) et phénogrammaire (c.a.d représentation de la surface d’un énoncé) de la langue, ex- primé par Curry ; et une modélisation algébrique du principe de compositionnalité afin de rendre compte de la sémantique des phrases, due à Montague. Un des avantages principaux de ce formalisme est que l’analyse d’une grammaires catégorielle abstraite permet de résoudre aussi bien le problème de l’analyse de texte, que celui de la génération de texte. Des algorithmes d’analyse efficaces ont été découverts pour les grammaires catégorielles abstraites de termes linéaires et quasi-linéaires, alors que le problème de l’analyse est non-élémentaire dans sa forme la plus générale. Nous proposons d’étudier des classes de termes pour lesquels l’analyse grammaticale reste solvable en temps polynomial. Ces résultats s’appuient principalement sur deux théorèmes de typage : le théorème de cohérence, spécifiant qu’un λ-terme donné est l’unique habitant d’un certain typage ; et le théorème d’expansion du sujet, spécifiant que deux termes β-équivalents habitent les même typages. Afin de mener cette étude à bien, nous utiliserons une représentation abstraite des notions de λ-termes et de typages, sous forme de jeux. En particulier, nous nous appuierons grandement sur cette notion afin de démontrer le théorème de cohérence pour de nouvelles familles de λ-termes et de typages. Grâce à ces résultats, nous montrerons qu’il est possible de construire de manière directe, un reconnaisseur dans le langage Datalog, pour des grammaires catégorielles abstraites de -termes quasi-affines. / Abstract categorial grammars (or, equivalently, lambda-grammars) is formalism based on the simply-typed lambda-calculus. These grammars can be described as grammars of such terms and were introduced in order to bring a model of the syntax-semantics interface in natural language, based on two main ideas: the distinction between the tectogrammatical (i.e. the deep structure of an utterance) and phenogrammatical (i.e. the interpretation of this structure) levels in natural languages, which was expressed by Curry; and an algebraic modeling of the principle of compositionality in order to give account of the semantics of a sentence. an idea formalized by Montague. One of the main advantages of abstract categorial grammars is that both the problems of natural language parsing and generation can be tackled under the same problem: parsing abstract categorial grammars. Efficient algorithms were discovered for abstract categorial grammars of linear and almost linear lambda-terms, while it is known the recognition problem is decidable but non-elementary in general. This work focuses on the study of classes of terms for which parsing can still be solved in polynomial time. The results we give are mainly based on two theorems: the coherence theorem which specifies that a given lambda-term in the desired class must be the unique inhabitant of one of its typing; and the subject expansion theorem, which states that two beta-equivalent terms of the desired class must inhabit the same typings. In order to lead the study, we use an alternative representation of both simply-typed lambda-terms and their typings as games. In particular, we will use this representation in order to prove the coherence theorems for new classes of lambda-terms. Thanks to these results, we will show it is possible to build in a direct way, recognizers for grammars of almost affine lambda-terms as Datalog programs.