Au cours des dernières années, les assistants de preuves on fait des progrès considérables et ont atteint un grand niveau de maturité. Ils ont permit la certification de programmes complexes tels que des compilateurs et même des systèmes d'exploitation. Néanmoins, l'utilisation d'un assistant de preuve requiert des compétences techniques très particulières, qui sont très éloignées de celles requises pour programmer de manière usuelle. Pour combler cet écart, nous entendons concevoir un langage de programmation de style ML supportant la preuve de programmes. Il combine au sein d'un même outil la flexibilité de ML et le fin niveau de spécification offert par un assistant de preuve. Autrement dit, le système peut être utilisé pour programmer de manière fonctionnelle et fortement typée tout en autorisant l'obtention de nouvelles garanties au besoin.On étudie donc un langage en appel par valeurs dont le système de type étend une logique d'ordre supérieur. Il comprend un type égalité entre les programmes non typés, un type de fonction dépendant, la logique classique et du sous-typage. La combinaison de l'appel par valeurs,des fonctions dépendantes et de la logique classique est connu pour poser des problèmes de cohérence. Pour s'assurer de la correction du système (cohérence logique et sûreté à l'exécution), on propose un cadre théorique basé sur la réalisabilité classique de Krivine. La construction du modèle repose sur une propriété essentielle qui lie les différent niveaux d'interprétation des types d'une manière novatrice.On démontre aussi l'expressivité de notre système en se basant sur son implantation dans un prototype. Il peut être utilisé pour prouver des propriétés de programmes standards tels que la fonction « map »sur les listes ou le tri par insertion. / In recent years, proof assistant have reached an impressive level of maturity. They have led to the certification of complex programs such as compilers and operating systems. Yet, using a proof assistant requires highly specialised skills and it remains very different from standard programming. To bridge this gap, we aim at designing an ML-style programming language with support for proofs of programs, combining in a single tool the flexibility of ML and the fine specification features of a proof assistant. In other words, the system should be suitable both for programming (in the strongly-typed, functional sense) and for gradually increasing the level of guarantees met by programs, on a by-need basis.We thus define and study a call-by-value language whose type system extends higher-order logic with an equality type over untyped programs, a dependent function type, classical logic and subtyping. The combination of call-by-value evaluation, dependent functions and classical logic is known to raise consistency issues. To ensure the correctness of the system (logical consistency and runtime safety), we design a theoretical framework based on Krivine's classical realisability. The construction of the model relies on an essential property linking the different levels of interpretation of types in a novel way.We finally demonstrate the expressive power of our system using our prototype implementation, by proving properties of standard programs like the map function on lists or the insertion sort.

La vérification automatique de preuves consiste à faire vérifier par un ordinateur la validité de démonstrations d'énoncés mathématiques. Cette vérification étant purement calculatoire, elle offre un haut degré de confiance. Elle est donc particulièrement utile pour vérifier qu'un logiciel critique, c'est-à-dire dont le bon fonctionnement a un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens, correspond exactement à sa spécification. DEDUKTI est l'un de ces vérificateurs de preuves. Il implémente un système de type, le lambda-Pi-Calcul Modulo, qui est une extension du lambda-calcul avec types dépendants avec des règles de réécriture du premier ordre. Suivant la correspondance de Curry-Howard, DEDUKTI implémente à la fois un puissant langage de programmation et un système logique très expressif. Par ailleurs, ce langage est particulièrement bien adapté à l'encodage d'autres systèmes logiques. On peut, par exemple, importer dans DEDUKTI des théorèmes prouvés en utilisant d'autres outils tels que COQ, HOL ou encore ZENON, ouvrant ainsi la voie à l'interopérabilité entre tous ces systèmes. Le lambda-Pi-Calcul Modulo est un langage très expressif. En contrepartie, certaines propriétés fondamentales du système, telles que l'unicité des types ou la stabilité du typage par réduction, ne sont pas garanties dans le cas général et dépendent des règles de réécriture considérées. Or ces propriétés sont nécessaires pour garantir la cohérence des systèmes de preuve utilisés, mais aussi pour prouver la correction et la complétude des algorithmes de vérification de types implémentés par DEDUKTI. Malheureusement, ces propriétés sont indécidables. Dans cette thèse, nous avons donc cherché à concevoir des critères garantissant la stabilité du typage par réduction et l'unicité des types et qui soient décidables, de manière à pouvoir être implémentés par DEDUKTI. Pour cela, nous donnons une nouvelle définition du lambda-Pi-Calcul Modulo qui rend compte de l'aspect itératif de l'ajout des règles de réécriture dans le système en les explicitant dans le contexte. Une étude détaillée de ce nouveau calcul permet de comprendre qu'on peut ramener le problème de la stabilité du typage par réduction et de l'unicité des types à deux propriétés plus simples, qui sont la compatibilité du produit et le bon typage des règles de réécriture. Nous étudions donc ces deux propriétés séparément et en donnons des conditions suffisantes effectives. Ces idées ont été implémentées dans DEDUKTI, permettant d'augmenter grandement sa généralité et sa fiabilité. / Automatic proof checking is about using a computer to check the validity of proofs of mathematical statements. Since this verification is purely computational, it offers a high degree of confidence. Therefore, it is particularly useful for checking that a critical software, i.e., a software that when malfunctioning may result in death or serious injury to people, loss or severe damage to equipment or environmental harm, corresponds to its specification. DEDUKTI is such a proof checker. It implements a type system, the lambda-Pi-Calculus Modulo, that is an extension of the dependently-typed lambda-calculus with first-order rewrite rules. Through the Curry-Howard correspondence, DEDUKTI implements both a powerful programming language and an expressive logical system. Furthermore, this language is particularly well suited for encoding other proof systems. For instance, we can import in DEDUKTI theorems proved using other tools such as COQ, HOL or ZENON, a first step towards creating interoperability between these systems.The lambda-Pi-Calculus Modulo is a very expressive language. On the other hand, some fundamental properties such as subject reduction (i.e., the stability of typing by reduction) and uniqueness of types are not guaranteed in general and depend on the rewrite rules considered. Yet, these properties are necessary for guaranteeing the coherence of the proof system, but also for provingthe soundness and completeness of the type-checking algorithms implemented in DEDUKTI. Unfortunately, these properties are undecidable. In this thesis, we design new criteria for subject reduction and uniqueness of types that are decidable in order to be implemented in DEDUKTI.For this purpose, we give a new definition of the lambda-Pi-Calculus Modulo that takes into account the iterative aspect of the addition of rewrite rules in the typing context. A detailed study of this new system shows that the problems of subject reduction and uniqueness of types can be reduced to two simpler properties that we call product compatibility and well-typedness of rewrite rules.Hence, we study these two properties separately and give effective sufficient conditions for them to hold.These ideas have been implemented in DEDUKTI, increasing its generality and reliability.

Le travail présenté dans cette thèse concerne l'étude de la notion de conversion inhérente à tous système de types dépendants. Plusieurs présentations de ces systèmes ont été étudiées pour des usages variés: typage, recherche de preuve, cohérence de logique... Chacune de ces représentation est accompagnée d'une notion d'égalité différente, suivant les besoins du moment. Mais il n'est pas certains que toutes ces représentations parlent en fin de compte d'une seule et même logique. Nous nous intéressons ici à une famille assez conséquente de systèmes de types, appelés Systèmes de Types Purs, et nous allons prouver que pour ces systèmes, toutes les représentations habituellement utilisées sont en fait équivalentes, c'est à dire qu'il existe des traductions constructives entre chacune de ces présentations. Ces traductions reposent toutes sur la manière de porter une égalité d'un système à l'autre. Ce travail se concentre donc sur les mécanismes de ces égalités, et prouve qu'il est possible de typer n'importe quelle égalité syntaxique en égalité sémantique, et ainsi qu'il est donc possible de passer d'un système à l'autre. L'intégralité de cette thèse a en outre été vérifiée et certifiée correcte à l'aide de l'assistant à la preuve Coq, qui a activement été utilisé tout au long de l'élaboration des preuves. ~

En génie logiciel, les méthodes modernes de développement (ex. le MDA) s'appuient de manière cruciale sur les notions de modélisation et de transformation. Ces méthodes peuvent s'interpréter à l'aide de la théorie des graphes. La difficulté théorique réside aujourd'hui dans l'ajout sur ces graphes de données supplémentaires sur lesquelles il est nécessaire de pouvoir effectuer des calculs. Notre travail s'est focalisé sur le développement d'un cadre mathématique sûr afin d'appliquer ces transformations. Les théories des catégories (à travers le double pushout) et des types inductifs (fonctions de calcul très expressives) nous ont permis de donner une solution unifiée à ce problème dans laquelle une seule opération permet de travailler sur la structure et de calculer avec les attributs en définissant des fonctions entre graphes possédant une partie contravariante pour le travail sur les attributs. De plus, les propriétés usuelles des systèmes de récriture sont vérifiées.

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.

Cette thèse présente une coopération entre l'assistant de preuve Coq et certains prouveurs externes basée sur l'utilisation de traces de preuves. Nous étudions plus particulièrement deux types de prouveurs pouvant renvoyer des certicats : d'une part, les réponses des prouveurs SAT et SMT peuvent être vériées en Coq afin d'augmenter à la fois la confiance qu'on peut leur porter et l'automatisation de Coq ; d'autre part, les théorèmes établis dans des assistants de preuves basés sur la Logique d'Ordre Supérieur peuvent être exportés en Coq et re-vérifiés, ce qui permet d'établir des preuves formelles mêlant ces deux paradigmes logiques. Cette étude a abouti à deux logiciels : SMTCoq, une coopération bi-directionnelle entre Coq et des prouveurs SAT/SMT, et HOLLIGHTCOQ, un outil important les théorèmes de HOL Light en Coq. L'architecture de chacun de ces deux développements a été pensée de manière modulaire et efficace, en établissant une séparation claire entre trois composants: un encodage en Coq du formalisme de l'outil externe qui est ensuite traduit avec soin vers des termes Coq, un vérificateur certifié pour établir les preuves, et un pré-processeur écrit en Ocaml traduisant les traces venant de prouveurs différents dans le même format de certicat. Grâce à cette séparation, un changement dans le format de traces n'affecte que le pré-processeur, sans qu'il soit besoin de modier du code ou des preuves Coq. Un autre composant essentiel pour l'efficacité et la modularité est la réflexion calculatoire, qui utilise les capacités de calcul de Coq pour établir des preuves à la fois courtes et génériques à partir des certificats.

Cette thèse traite deux problèmes concernant la théorie des représentations `-modulairesd’un groupe p-adique. Soit F un corps local non archimédien de caractéristique résiduelle pdifférente de `. Dans la première partie, on étudie la décomposition en blocs de la catégoriedes représentations lisses `-modulaires de GL(n; F) et de ses formes intérieures. On veutramener la description d’un bloc de niveau positif à celle d’un bloc de niveau 0 (d’un autregroupe du même type) en cherchant des équivalences de catégories. En utilisant la théoriedes types de Bushnell-Kutzko dans le cas modulaire et un théorème de la théorie descatégories, on se ramene à trouver un isomorphisme entre deux algèbres d’entrelacement.La preuve de l’existence d’un tel isomorphisme n’est pas complète car elle repose sur uneconjecture qu’on énonce et qui est prouvée pour plusieurs cas. Dans une deuxième partieon généralise la construction du groupe métaplectique et de la représentation de Weil dansle cas des représentations sur un anneau intègre. On construit une extension centrale dugroupe symplectique sur F par le groupe multiplicatif d’un anneau intègre et on prouvequ’il satisfait les mêmes propriétés que dans le cas des représentations complexes. / This thesis focuses on two problems on `-modular representation theory of p-adic groups.Let F be a non-archimedean local field of residue characteristic p different from `. In thefirst part, we study block decomposition of the category of smooth modular representationsof GL(n; F) and its inner forms.We want to reduce the description of a positive-levelblock to the description of a 0-level block (of a similar group) seeking equivalences of categories.Using the type theory of Bushnell-Kutzko in the modular case and a theorem ofcategory theory, we reduce the problem to find an isomorphism between two intertwiningalgebras. The proof of the existence of such an isomorphism is not complete because itrelies on a conjecture that we state and we prove for several cases. In the second part wegeneralize the construction of metaplectic group and Weil representation in the case ofrepresentations over un integral domain. We define a central extension of the symplecticgroup over F by the multiplicative group of an integral domain. We prove that it satisfiesthe same properties as in the complex case.

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