Marie Kerjean

Soutenance de thèse

La soutenance de ma thèse s'est déroulée le Vendredi 19 Octobre 2018, devant un Jury composé de :

Thomas Ehrhard & Directeur de thèse
Tom Hirschowitz & Rapporteur
Prakash Panangaden & Rapporteur (Absent)
Paul-André Melliès & Examinateur
Mai Gehrke & Examinatrice
Samuel Mimram & Examinateur
Christine Tasson & Examinatrice

Vous trouverez ici le manuscript et les transparents .

Résumé

Espaces réflexifs de fonctions lisses: un compte rendu logique des équations aux dérivées partielles linéaires.

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 ceux-ci comme des fonctions entre les types, et permet en retour d’affiner notre compréhension des preuves/programmes. La logique linéaire (LL) donne une interprétation logique des notions d’algèbre linéaire, quand la logique linéaire différentielle (DiLL) 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. 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 types négatifs 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.

Reflexive spaces of smooth functions: a logical account of linear partial differential equations.

Around the Curry-Howard 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 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.