La théorie de la preuve se développe depuis la correspondance de Curry-Howard suivant deux sources d’inspirations : les langages de programmation, pour lesquels elle agit comme une théorie des types de données, et l’étude sémantique des preuves. Cette dernière consiste à donner des modèles mathématiques pour les comportements des preuves/programmes. En particulier, la sémantique dénotationnelle s’attache à interpréter les deux-ci comme des fonctions entre des types, et permet en retour d’affiner notre compréhension des preuves/programmes. La logique linéaire (LL), introduite par Girard, donne une interprétation logique des notions d’algèbre linéaire, quand la logique linéaire différentielle (DiLL), introduite par Ehrhard et Regnier, permet une compréhension logique de la notion de différentielle.Cette thèse s’attache à renforcer la correspondance sémantique entre théorie de la preuve et analyse fonctionnelle, en insistant sur le caractère involutif de la négation dans DiLL.La première partie consiste en un rappel des notions de linéarité, polarisation et différentiation en théorie de la preuve, ainsi qu’un exposé rapide de théorie des espaces vectoriels topologiques. La deuxième partie donne deux modèles duaux de la logique linéaire différentielle, interprétant la négation d’une formule respectivement par le dual faible et le dual de Mackey. Quand la topologie faible ne permet qu’une interprétation discrète des preuves sous forme de série formelle, la topologie de Mackey nous permet de donner un modèle polarisé et lisse de DiLL, et de raffiner des résultats précédemment obtenus par Blute, Dabrowski, Ehrhard et Tasson. Enfin, la troisième partie de cette thèse s’attache à interpréter les preuves de DiLL par des distributions à support compact. Nous donnons un modèle polarisé de DiLL où les formules négatives sont interprétés par des espaces Fréchet Nucléaires. Nous montrons que enfin la résolution des équations aux dérivées partielles linéaires à coefficients constants obéit à une syntaxe qui généralise celle de DiLL, que nous détaillons. / Around the curry-coward correspondence, proof-theory has grown along two distinct fields : the theory of programming languages, for which formulas acts as data types, and the semantic study of proofs. The latter consists in giving mathematical models of proofs and programs. In particular, denotational semantics distinguishes data types which serves as input or output of programs, and allows in return for a finer understanding of proofs and programs. Linear Logic (LL) gives a logical interpretation of the basic notions from/of linear algebra, while Differential Linear Logic allows for a logical understanding of differentiation. This manuscript strengthens the link between proof-theory and functional analysis, and highlights the role of linear involutive negation in DiLL. The first part of this thesis consists in a quick overview of prerequisites on the notions of linearity, polarisation and differentiation in proof-theory, and gives the necessary background in the theory of locally convex topological vector spaces. The second part uses two classic topologies on the dual of a topological vector space and gives two models of DiLL: the weak topology allows only for a discrete interpretation of proofs through formal power series, while the Mackey topology on the dual allows for a smooth and polarised model of DiLL. Finally, the third part interprets proofs of DiLL by distributions. We detail a polarized model of DiLL in which negatives are Fréchet Nuclear spaces, and proofs are distributions with compact support. We also show that solving linear partial differential equations with constant coefficients can be typed by a syntax similar to the one of DiLL, which we detail.

Si l'interet et l'efficacite des methodes d'analyse statique par interpretation abstraite pour la verification des programmes critiques embarques ne sont plus a demontrer, il est maintenant necessaire d'obtenir des methodes les plus precises possibles. Si l'utilisation de domaines abstraits relationnels de plus en plus elabores permet de diminuer la surapproximation dont souffre les domaines les plus simples, les analyses actuelles souffrent toujours d'une mauvais prise en compte des entrees du programme. Ces entrees sont fournies par un capteur qui mesure une grandeur physique, et sont generalement surapproximees par un intervalle. Une piste d'etude recente pour mieux gerer ces entrees continues consiste a etudier, outre le programme lui-meme, l'environnement physique dans lequel il est execute. On obtient ainsi un systeme plus complexe comprenant une dynamique discrete (le programme) et une dynamique continue (l'environnement). L'etude de tels systemes hybrides repose actuellement essentiellement sur des extensions des automates a etats finis et des algebres de processus introduisant une dynamique continue. L'analyse de ces systemes par des techniques de model-checking souffre encore d'une explosion combinatoire excluant leur utilisation pour les logiciels embarques critiques les plus gros. La premiere contribution de cette these est une extension des langages de programmation imperatifs permettant de d´ecrire a la fois le programme, l'environnement exterieur et les interactions entre le programme et l'environnement. L'environnement physique est d´ecrit par un ensemble d'equations differentielles representant chacune un mode continu, et les interactions entre le programme et l'exterieur sont modelises par deux mots cles representant les capteurs et actionneurs. Nous donnons a l'ensemble (programme plus environnement physique) une semantique denotationnelle qui reste tres proche de celle definie pour les langages imperatifs classiques. La difficulte majeure dans la construction de cette semantique a ete de definir une semantique pour la partie continue : les solutions des equations diff´erentielles sont exprimees comme le plus petit point fixe d'un operateur monotone dans un CPO, et nous montrons que les iterees de Kleene convergent vers ce point fixe. La seconde contribution est une methode d'analyse statique par interpretation abstraite de ces systemes hybrides. Cette methode fonctionne en deux temps. Tout d'abord, sous certaines restrictions portant sur le programme a analyser, on construit un recouvrement de l'espace des variables d'entree via une analyse par intervalle couplee a une analyse d'atteignabilite en avant. On obtient ainsi une abstraction de l'impact qu'a le programme sur l'evolution continue : l'espace d'entree du programme est d´coupe en zones dans lesquelles on est sur qu'un actionneur sera active. Dans un deuxieme temps, nous utilisons ce recouvrement et une methode d'integration garantie des equations differentielles pour obtenir une surapproximation de l'evolution continue. Un analyseur prototype implementant ces techniques a ete developpe et les tests sur les exemples classiques de systemes hybrides montrent de bons resultats. Enfin, la troisieme contribution de cette these est une nouvelle methode d'integration garantie nommee GRKLib. Contrairement aux methodes existantes, GRKLib se fonde sur un schema d'integration numerique non garantie (nous avons choisi un schema de Runge-Kutta d'ordre 4, mais n'importe quelle autre convient) et nous calculons, en utilisant l'arithmetique d'intervalles, l'erreur globale commise lors de l'integration numerique. Cette erreur s'exprime comme la somme de trois termes : l'erreur sur un pas, la propagation de l'erreur et l'erreur due aux nombres flottants. Chaque terme est calcule separement et des techniques avancees permettent de les reduire et de controler au mieux le pas d'integration pour limiter l'accroissement de l'erreur globale. Une librairie C++ implementant ces concepts a ete developpee, et les resultats presentes dans cette these sont prometteurs.

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 présente différentes notions d'observation en sémantique, et quelques résultats sur leurs relations. Après avoir rappelé les définitions du lambda-calcul simplement typé et de ses modèles, nous présentons la notion d'observation définie par un modèle. Dans une première partie, nous présentons les liens entre cette notion et la définissabilité relative, en prenant les exemples de PCF unaire, de PCF finitaire et du modèle fortement stable de PCF, en étendant des travaux de Bucciarelli, Malacaria et Longley.<br />La partie suivante est consacrée à l'étude de la notion d'observation dans le cadre d'un langage avec des effets de bord. Nous proposons un modèle basé sur les domaines de Fraenkel-Mostowski, sur lequel nous définissons des relations logiques pour prouver des équivalences, aui servent à distinguer la partie publique de la mémoire de la partie secrète où les invariants sont préservés; ce qui établit un lien avec les problématiques de sécurité.<br />Enfin, nous étudions la question du temps d'exécution en sémantique dénotationnelle. Nous proposons une construction axiomatique, basée sur une monade, pour représenter le te,ps d'exécution sans le rendre observable par le contexte. Nous appliquons cette construction au modèle des espaces de cohérence et aux jeux de Hyland et Ong. Nous prouvons que ce dernier modèle est complètement adéquat.

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).

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.

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.

La sémantique des jeux est une sémantique dénotationnelle centrée sur l’interaction : preuves et programmes y sont représentés par des stratégies modélisant, par le flot d’exécution, leur manière de réagir à leur environnement. Malgré cette présentation intensionnelle, les sémantiques de jeux ne suffisent pas à capturer certaines informations calculatoires annexes au flot d’exécution telles que, par exemple, la production de témoins en logique du premier ordre ou la consommation de ressources dans les langages de programmation. Dans cette thèse nous proposons un enrichissement du modèle des jeux concurrent à base de structures d’événements permettant de garder trace de ces informations.Nous construisons d’abord un modèle de jeux concurrent dans lequel les coups joueurs d’une stratégie sont annotés par les termes d’une théorie (in)équationnelle. Cette théorie est un paramètre de notre modèle et les annotations permettent de refléter de manière compacte des informations d’exécution n’ayant pas d’influence sur le flot d’exécution. Nous montrons que le modèle ainsi construit préserve la structure catégorique compacte fermée du modèle sans annotation.Nous explorons ensuite l’expressivité de notre modèle et présentons deux interprétations nouvelles en sémantique des preuves et des programmes : l’une interprétant les preuves de la logique classique du premier ordre par des stratégies concurrentes avec échange de témoins, donnant une version compositionnelle au théorème de Herbrand ; l’autre permettant de refléter les aspects quantitatifs liés à la consommation de ressources telles que le temps, dans l’exécution de programmes concurrents d’ordre supérieur avec mémoire partagée. / This thesis presents a general framework for enriching causal concurrent games model with annotations. These annotations can be viewed as meta-data on strategies: they are modified throughout interactions but do not affect their general flow of control. These data can be of various nature, in particular our enrichment is parametrised over any multi-sorted equational theory and can also reflect structure upon these data such as a partial order. From a semantics point of view, this construction is motivated by problems from both logic and programming languages: On the logic side, the annotated games model specialised to first-order terms enables us to give a novel interpretation of first-order classical proofs as concurrent strategies carrying first-order witnesses. In particular this answer the question of giving a compositional version to Herbrand’s theorem while avoiding the usual proof sequentialization of other denotational approaches. On the programming language side, annotations on games offer intrinsic quantitative models. We show that those can be used to provide denotational semantics for resource consumption analysis of concurrent higher order programming language with shared memory.These enrichments, strongly connected to the causal structure of concurrent games, give an argument in favor of a causal meaning of computations.