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.

Une bonne partie des résultats contenus dans ce travail portent sur les réseaux de démonstration de la logique linéaire ainsi que sur la sémantique des espaces cohérents. Ces résultats concernent plus particulièrement les variantes non commutatives de la logique linéaire que ce soit à la Lambek-Abrusci ou dans le calcul ordonné de l'auteur. Ils sont ensuite appliqués à la syntaxe du langage naturel, modélisée bien évidemment par les grammaires catégorielles, les TAGS, mais aussi par les grammaires minimalistes de Stabler que l'on peut aussi simuler en logique linéaire. Pour tous ces systèmes grammaticaux, le calcul de représentations sémantiques est explicité.

La confiance formelle en une propriété abstraite provient de l'existence d'une preuve de sa correction, qu'il s'agisse d'un théorème mathématique ou d'une qualité du comportement d'un logiciel ou processeur. Il existe de nombreuses définitions différentes de ce qu'est une preuve, selon par exemple qu'elle est écrite soit par des humains soit par des machines, mais ces définitions sont toutes concernées par le problème d'établir qu'un document représente en fait une preuve correcte. Le cadre des Certificats de Preuve Fondamentaux (Foundational Proof Certificates, FPC) est une approche proposée récemment pour étudier ce problème, fondée sur des progrès de la théorie de la démonstration pour définir la sémantique des formats de preuve. Les preuves ainsi définies peuvent être vérifiées indépendamment par un noyau vérificateur de confiance codé dans un langage de programmation logique. Cette thèse étend des résultats initiaux sur la certification de preuves du premier ordre en explorant plusieurs dimensions logiques essentielles, organisées en combinaisons correspondant à leur usage en pratique: d'abord, la logique classique sans points fixes, dont les preuves sont générées par des démonstrateurs automatiques de théorème; ensuite, la logique intuitionniste avec points fixes et égalité,dont les preuves sont générées par des assistants de preuve. Les certificats de preuve ne se limitent pas comme précédemment à servir de représentation des preuves complètes pour les vérifier indépendamment. Leur rôle s'étend pour englober des transformations de preuve qui peuvent enrichir ou compacter leur représentation. Ces transformations peuvent rendre des certificats plus simples opérationnellement, ce qui motive la construction d'une suite de vérificateurs de preuve de plus en plus fiables et performants. Une autre nouvelle fonction des certificats de preuve est l'écriture d'aperçus de preuve de haut niveau, qui expriment des schémas de preuve tels qu'ils sont employés dans la pratique des mathématiciens, ou dans des techniques automatiques comme le property-based testing. Ces développements s'appliquent à la certification intégrale de résultats générés par deux familles majeures de démonstrateurs automatiques de théorème, utilisant techniques de résolution et satisfaisabilité, ainsi qu'à la création de langages programmables de description de preuve pour un assistant de preuve. / Formal trust in an abstract property, be it a mathematical result or a quality of the behavior of a computer program or a piece of hardware, is founded on the existence of a proof of its correctness. Many different kinds of proofs are written by mathematicians or generated by theorem provers, with the common problem of ascertaining whether those claimed proofs are themselves correct. The recently proposed Foundational Proof Certificate (FPC) framework harnesses advances in proof theory to define the semantics of proof formats, which can be verified by an independent and trusted proof checking kernel written in a logic programming language. This thesis extends initial results in certification of first-order proofs in several directions. It covers various essential logical axes grouped in meaningful combinations as they occur in practice: first,classical logic without fixed points and proofs generated by automated theorem provers; later, intuitionistic logic with fixed points and equality as logical connectives and proofs generated by proof assistants. The role of proof certificates is no longer limited to representing complete proofs to enable independent checking, but is extended to model proof transformations where details can be added to or subtracted from a certificate. These transformations yield operationally simpler certificates, around which increasingly trustworthy and performant proof checkers are constructed. Another new role of proof certificates is writing high-level proof outlines, which can be used to represent standard proof patterns as written by mathematicians, as well as automated techniques like property-based testing. We apply these developments to fully certify results produced by two families of standard automated theorem provers: resolution- and satisfiability-based. Another application is the design of programmable proof description languages for a proof assistant.

Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.