Cette thèse est une étude de la géométrie de l'interaction dans le facteur hyperfini (GdI5), introduite par Jean-Yves Girard, et de ses liens avec les constructions plus anciennes. Nous commençons par montrer comment obtenir des adjonctions purement géométriques comme une identité entre des ensembles de cycles apparaissant entre des graphes. Il est alors possible, en choisis- sant une fonction qui mesure les cycles, d'obtenir une adjonction numérique. Nous montrons ensuite comment construire, sur la base d'une adjonction numérique, une géométrie de l'interaction pour la logique linéaire multiplicative additive où les preuves sont interprétées par des graphes. Nous expliquons également comment cette construction permet de définir une sémantique dénotationnelle de MALL, et une notion de vérité. Nous étudions finalement une généralisation de ce cadre utilisant des outils de théorie de la mesure afin d'interpréter les exponentielles et le second ordre. Les constructions sur les graphes étant paramétrées par une fonction de mesure des cycles, nous entreprenons ensuite l'étude de deux cas particuliers. Le premier s'avère être une version combinatoire de la GdI5, et nous obtenons donc une interprétation géométrique de l'orthogonalité basée sur le déterminant de Fuglede-Kadison. Le second cas particulier est une version combinatoire des constructions plus anciennes de la géométrie de l'interaction, où l'orthogonalité est basée sur la nilpotence. Ceci permet donc de comprendre le lien entre les différentes versions de la géométrie de l'interaction, et d'en déduire que les deux adjonctions -- qui semblent à première vue si différentes -- sont des conséquences d'une même identité géométrique. Nous étudions ensuite la notion de vérité subjective. Nous commençons par considérer une version légè- rement modifiée de la GdI5 avec une notion de vérité dépendant du choix d'une sous-algèbre maximale commutative (masa). Nous montrons qu'il existe une correspondance entre la classification des masas introduite par Dixmier (regulière, semi-régulière, singulière) et les fragments de la logique linéaire que l'on peut interpréter dans cette géométrie de l'interaction. Nous étudions alors la vérité subjective de la GdI5, qui dépends du choix d'une représentation du facteur hyperfini de type II1, à la lumière de ce résultat. Finalement, nous détaillerons une proposition de Girard pour étudier les classes de complexité et dé- taillons la caractérisation obtenue par ce dernier de la classe de complexité co-NL, en montrant comment coder un problème complet pour cette classe à l'aide d'opérateurs.

Le langage d'assignation statique unique, SSA, est l'une des représentations intermédiaires les plus communément utilisées dans les compilateurs industriels. Cependant l'intérêt de la communauté d'analyse statique de programmes est minime, un fait dû aux faibles fondations formelles du langage SSA. Cette thèse présente une sémantique dénotationelle du langage SSA, permettant des définitions formelles des analyses statiques du langage SSA en se basant sur les méthodes classiques de l'interprétation abstraite. D'un point de vue pratique, cette thèse présente l'implémentation des analyseurs statiques définis formellement dans un compilateur industriel, la Collection de Compilateurs GNU, GCC.

Cette thèse est une étude de la géométrie de l'interaction dans le facteur hyperfini (GdI5), introduite par Jean-Yves Girard, et de ses liens avec les constructions plus anciennes. Nous commençons par montrer comment obtenir des adjonctions purement géométriques comme une identité entre des ensembles de cycles apparaissant entre des graphes. Il est alors possible, en choisissant une fonction qui mesure les cycles, d'obtenir une adjonction numérique. Nous montrons ensuite comment construire, sur la base d'une adjonction numérique, une géométrie de l'interaction pour la logique linéaire multiplicative additive où les preuves sont interprétées par des graphes. Nous expliquons également comment cette construction permet de définir une sémantique dénotationnelle de MALL, et une notion de vérité. Nous étudions finalement une généralisation de ce cadre afin d'interpréter les exponentielles et le second ordre. Les constructions sur les graphes étant paramétrées par une fonction de mesure des cycles, nous entreprenons ensuite l'étude de deux cas particuliers. Le premier s'avère être une version combinatoire de la GdI5, et nous obtenons donc une interprétation géométrique de l'orthogonalité basée sur le déterminant de Fuglede-Kadison. Le second cas particulier est une version combinatoire des constructions plus anciennes de la géométrie de l'interaction, où l'orthogonalité est basée sur la nilpotence. Ceci permet donc de comprendre le lien entre les différentes versions de la géométrie de l'interaction, et d'en déduire que les deux adjonctions — qui semblent à première vue si différentes — sont des conséquences d'une même identité géométrique. / This work is a study of the geometry of interaction in the hyperfinite factor introduced by Jean-Yves Girard, and of its relations with ancient constructions. We start by showing how to obtain purely geometrical adjunctions as an identity between sets of cycles appearing between graphs. It is then possible, by chosing a function that measures those cycles, to obtain a numerical adjunction. We then show how to construct, on the basis of such a numerical adjunction, a geometry of interaction for multiplicative additive linear logic where proofs are interpreted as graphs. We also explain how to define from this construction a denotational semantics for MALL, and a notion of truth. We extend this setting in order to deal with exponential connectives and show a full soundness result for a variant of elementary linear logic (ELL). Since the constructions on graphs we define are parametrized by a function that measures cycles, we then focus our study to two particular cases. The first case turns out to be a combinatorial version of GoI5, and we thus obtain a geometrical caracterisation of its orthogonality which is based on Fuglede-Kadison determinant. The second particular case we study will giveus a refined version of older constructions of geometry of interaction, where orthogonality is based on nilpotency. This allows us to show how these two versions of GoI, which seem quite different, are related and understand that the respective adjunctions are both consequences of a unique geometrical property. In the last part, we study the notion of subjective truth.