Search

In this thesis, I study several possibilities to extend intuitionistic type theory with extensionality principles, such as function extensionality or Voevodsky's univalence axiom, while preserving the computational properties of the proofs. In the first part, I develop a complete meta-theory for the observational equality of Altenkirch et al. In particular, I obtain a formal proof of normalization, canonicity and decidability of the conversion for an observational type theory with impredicative proof-irrelevant propositions. Then in a second part, I sketch a translation from homotopy type theory to observational type theory based on the model of Coquand et al in cubical sets. Finally, in the last part I explain how to take advantage of the computational properties of cubical type theory to obtain elegant synthetic proofs of classical results from homotopy theory, in particular the construction of the Hopf fibration and the 3x3 lemma for homotopy pushouts.; Dans cette thèse, j'étudie plusieurs manières d'étendre la théorie des types intuitionniste avec des principes d'extensionnalité, comme par exemple l'extensionnalité des fonctions ou l'axiome d'univalence de Voevodsky, en portant une attention particulière à la préservation des propriétés calculatoires des preuves. Dans une première partie, je développe une méta-théorie complète pour l'égalité observationnelle de Altenkirch et al. J'obtiens notamment une preuve formelle de normalisation, de canonicité et de décidabilité de la conversion pour une théorie des types observationnelle avec des propositions imprédicatives. Dans une seconde partie, j'esquisse une traduction de la théorie des types homotopique vers la théorie des types observationnelle, en me basant sur le modèle cubique de Coquand et al. Enfin dans une dernière partie, j'explique comment tirer parti des propriétés calculatoires de la théorie des types cubique pour obtenir des preuves synthétiques élégantes de résultats classiques de la théorie de l'homotopie, notamment la construction de la fibration de Hopf et le lemme 3x3 pour les sommes amalgamées homotopiques.

This thesis investigates the use of type theories and types with regards to compositionality in the formal semantic models of computational linguistics. Semantic types play a fundamental role in the detection and representation of semantic phenomena such as creative uses of language, polysemy and copredication. As a consequence, a formal account of types requires linguistic accuracy as well as theoretical mechanisms to manipulate complex structures and type coercions. In order to meet these expectations, the present thesis aims to propose a minimalist account of the construction of semantic type theories which would make it possible to unify the various current approaches to formal and lexical semantics. A first part is dedicated to the study of the linguistic constraints which influence the notion of semantic type itself, and leads to the formulation of general principles to supervise the production of semantic type theories. In a second part, these principles are interpreted in the light of the mathematical foundations of such theories, leading to the construction of a Montagovian-style type theory with subtyping and coercions from a topos as a categorical model. Finally, a third and last part deals with the choice of base semantic types in order to determine experimentally whether such types can be acquired from empirical data., Cette thèse s’intéresse à l’utilisation des théories de types et des types eux-mêmes dans les formalismes sémantiques compositionnels en traitement automatique des langues. Les types sémantiques jouent un rôle essentiel dans la détection et la représentation de certains phénomènes sémantiques, incluant les usages créatifs de la langue, la polysémie et la coprédication, et nécessitent pour cela une certaine précision linguistique ainsi que des mécanismes théoriques capable de manipuler des structures complexes et des coercions de types. Afin de répondre à ces exigences, l’objectif de ce travail de thèse est de proposer une base minimaliste à la construction des théories de types sémantiques, qui soit capable dans une certaine mesure d’unifier les différentes approches actuelles à la sémantique lexicale et formelle. Une première partie est dédiée à l’examen des contraintes linguistiques qui pèsent sur la notion même de type sémantique, et aboutit à l’élaboration de principes généraux destinés à encadrer l’élaboration de théories de types sémantiques. Dans une seconde partie, ces principes sont confrontés aux fondements mathématiques de telles théories, conduisant à la construction d’une théorie de types dans un style montagovien, augmenté d’une relation de sous-typage et de coercions, à partir d’un modèle catégorique de topos. Enfin, une dernière partie traite du choix des types sémantiques de base, et tente d’évaluer expérimentalement si l’acquisition de tels types à partir de données empiriques est envisageable.

Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to gain more time and effort for the users. This thesis presents three contributions associated with the integration of automated provers in proof assistants. The first contribution consists of the implementation of a tactic that calls automated provers from Lambdapi by using an external platform called Why3. Usually, automated provers do not generate a complete certificate of a given formula, thus, the second contribution presented in this thesis is the reconstruction in Lambdapi of proofs generated by first-order automated provers implemented in a tool called Ekstrakto. Finally, automated provers often perform some transformations on the formula that they are trying to solve. Among these transformations, we can find Skolemization steps. The last contribution is devoted to the certification of Skolemization steps performed by the automated provers in order to have a complete reconstruction. This has been implemented in a tool called Skonverto.; Lambdapi est un assistant de preuve qui permet à l’utilisateur la construction d’une preuve d’un théorème donné dans un langage universel basé sur le lambda-pi-calcul. Le but de cette thèse est de rajouter de l’automatisation à Lambdapi pour faire gagner du temps à l’utilisateur. Cette thèse présente trois contributions liées à l’intégration des démonstrateurs automatiques dans les assistants de preuve. La première contribution consiste en l’implémentation d’une tactique qui fait appel au démonstrateurs automatiques depuis Lambdapi à travers une plateforme tiers appelé Why3. Généralement, les démonstrateurs automatiques ne génèrent pas un certificat de preuve complet, d’où la deuxième contribution présentée dans cette thèse: la reconstruction de preuves générées par les démonstrateurs automatiques du premier ordre dans Lambdapi implémenté dans un outil appelé Ekstrakto. Enfin, ces démonstrateurs peuvent parfois effectuer des modifications sur la formule qu'ils sont en train de prouver. Le dernier résultat de la thèse est consacré à la certification des étapes de Skolemisation faites par les démonstrateurs automatiques. Un algorithme est présenté, montré correct et impleménté dans l'outil Skonverto.

Dedukti is a logical framework in which the user encodes the theory she wantsto use via rewriting rules. To ensure the decidability of typing, the rewriting system must be terminating.After recalling some properties of pure type systems and their extension with rewriting, a termination criterion for higher-order rewriting with dependent types is presented. It is an extension of the dependency pairs to the lambda-pi-calculus modulo rewriting. This result features two main theorems. The first one states that the well-foundedness of the call relation defined from dependency pairs implies the strong normalization of the rewriting system.The second result of this part describes decidable sufficient conditions to use the first one. This decidable version of the termination criterion is implemented in “SizeChange Tool”.The second part of this thesis is dedicated to the use of the logical framework Dedukti to encode a rich type theory. We are interested in a fragment of the logic beyond Agda which includes two widely used features: extension of conversion with the eta rule and universe polymorphism.Once again, this work includes a theoretical part, with correct encodings of both features in the lambda-pi-calculus modulo rewriting, and a prototypical translator from Agda to Dedukti.; Dedukti est un cadre logique dans lequel l’utilisateur encode la théorie qu’il souhaite utiliser à l’aide de règles de réécriture. Pour garantir la décidabilité du typage, il faut s’assurer que le système de réécriture utilisé est terminant.Après avoir rappelé les propriétés des systèmes de types purs et leur extension avec de la réécriture, un critère de terminaison pour la réécriture d’ordre supérieur avec types dépendants est présenté. Il s’agit d’une extension de la notion de paires de dépendances au cas du lambda-pi-calcul modulo réécriture. Cerésultat se décompose en deux théorèmes principaux. Le premier stipule que la bonne fondaison de la relation d’appel définie à partir des paires de dépendances implique la normalisation forte du système de réécriture.Le second résultat de cette partie décrit des conditions décidables suffisantes pour pouvoir utiliser le premier théorème. Cette version décidable du critère de terminaison est implémenté dans un outil appelé “SizeChange Tool”.La seconde partie de cette thèse est consacrée à l’utilisation du cadre logiqueDedukti pour encoder une théorie des types riche. Nous nous intéressons plusparticulièrement à la traduction d’un fragment d’Agda incluant deux fonctionnalités très répandues : l’extension de la conversion avec la règle eta et le polymorphisme d’univers.Une fois encore, ce travail possède un versant théorique, avec des encodagesprouvés corrects de ces deux fonctionnalités dans le lambda-pi-calcul modulo réécriture, ainsi qu’une implémentation prototypique de traducteur entre Agda et Dedukti.

We study a type theoretic definition of weak omega-categories originally introduced by Finster and Mimram, inspired both from ideas coming from homotopy type theory and from a definition of weak omega-category due to Grothendieck and Maltsiniotis. The advantages of such an approach are multiple: The language of type theory allows for a definition restricted to only a few rules, it also provides an explicit syntax on which one can perform inductive reasoning, and gives an algorithm for implementing a proof-assistant dedicated to exploring weak omega-categories. The work we present about this type theory is organized along two main axes: We investigate the theoretical grounds for this definition and relate it to an other known definition of weak omega-categories, and we present the proof-assistant based on this theory together with practical considerations to improve its use. We also consider a generalization of this approach to other related higher structures.We start with an introduction to the language of dependent type theory that we rely on to introduce our definitions, presenting both the syntax and the semantics that we study by means of categorical tools. We then present weak omega-categories and a type theory that defines them. We detail the categorical semantics of this theory and our main contribution in this direction establishes an equivalence between its models and the prior definition of weak omega-categories due to Grothendieck and Maltsiniotis. This definition has enabled us to implement a proof-assistant capable of checking whether a given morphism is well-defined in the theory of weak omega-category, and we present this implementation together with a few examples demonstrating both the capabilities of such a tool, and its tediousness in the vanilla version. To improve this issue, we present two main additional features allowing to partially automating its use: The suspension and the functorialization. These two operations are defined by similar techniques of induction on the syntax of the type theory. We then generalize this definition of weak omega-categories and present a type theoretic framework that is both modular enough to allow for defining higher structures, and constrained enough to precisely understand its semantics. This enables us to sketch a connection with the theory of monads with arities. Using this framework, we introduce and study two other definitions of higher structures: Monoidal weak omega-categories and cubical weak omega-categories. By using syntactic reasoning we are able to defines translations back and forth between the type theory defining weak omega-categories and the one describing monoidal weak omega-categories. One of our main result is to show that these translations imply an equivalence at the level of models: It shows that the monoidal omega-categories are equivalent to the omega-categories with a single object thus justifying the correctness of the appellation monoidal. We then give an alternate presentation of the type theory defining monoidal weak omega-categories, which diverges from our framework but is more standalone, and prove it to be equivalent to the previous presentation. We finally introduce in our framework a definition of cubical weak omega-categories and study its semantics, our main result along these lines is to characterize the models of this type theory and extract a mathematical definition equivalent to them.; Nous présentons une définition des omega-catégories faibles formulée en théorie des types proposée initialement par Finster et Mimram, suivant des idées provenant à la fois de la théorie homotopique des types et d’une définition des omega-catégories faibles due à Grothendieck et Maltsiniotis. Les avantages d’une telle approche sont multiples : Le langage de la théorie des types permet une définition qui se réduit à quelques règles seulement, et il fournit une syntaxe explicite sur laquelle il est possible de raisonner par induction. Cela donne également un algorithme pour implémenter un assistant de preuve dédié à l’exploration des omega-catégories faibles. Le travail que nous présentons est organisé selon deux axes principaux : Nous étudions les fondements théoriques de cette définition et la relions aux autres définitions connues de omega-catégories faibles, et nous présentons l’assistant de preuve basé sur cette théorie avec des considérations pour rendre cet outil plus utilisable en pratique. Nous considérons également des généralisations de cette approche à d’autres structures supérieures similaires.Nous commençons par présenter une introduction à la théorie des types dépendants sur laquelle repose les définitions que nous étudions, en introduisant à la fois une syntaxe et sa sémantique catégorique. Nous présentons ensuite les omega-catégories faibles avec une théorie des types pour les définir. Nous détaillons la sémantique catégorique de cette théorie et notre contribution principale dans cette direction établit une équivalence entre les modèles de cette théorie et la définition antérieure des omega-catégories faibles due à Grothendieck et Maltsiniotis. Cette définition nous a permis d’implémenter un assistant de preuves capable de vérifier si un morphisme donné est correctement défini dans la théorie des omega-catégories faibles; nous présentons cette implémentation accompagnée de quelques exemples illustrant à la fois les possibilités de l’outil, et l’impraticabilité de son utilisation dans sa version native. Pour corriger ce problème, nous présentons deux fonctionnalités additionnelles permettant une automatisation partielle : La suspension et la fonctorialisation. Ces deux opérations sont définies par des techniques similaires, par induction sur la syntaxe de la théorie des types. Nous généralisons ensuite cette définition des omega-catégories faibles et présentons un cadre pour étudier des théories des types, qui est à la fois suffisamment modulaire pour permettre de définir d’autres structures supérieures, et suffisamment contraint pour étudier précisément sa sémantique. Cela nous permet d’esquisser une connexion avec la théorie des monades à arités. En se reposant sur ce cadre, nous introduisons et étudions deux autres définitions de structures supérieures : les omega-catégories faibles monoidales et les omega-catégories faibles cubiques. Par un raisonnement syntaxique, nous définissons des traductions dans les deux sens entre les théories des types qui définissent les omega-catégories faibles et les omega-catégories faibles monoidales. L’un de nos résultats principaux est de montrer que ces traductions induisent une équivalence au niveau des modèles, montrant que les omega-catégories faibles monoidales sont équivalentes aux omega-catégories qui ont un unique objet justifiant l’appellation de monoidal. Nous donnons ensuite une présentation alternative de la théorie des types pour définir les omega-catégories faibles monoidales, qui diverge de notre cadre, mais qui est plus indépendante, et la prouvons équivalente à la présentation précédente. Finalement nous introduisons dans notre cadre une définition de la théorie des omega-catégories faibles cubiques, et étudions sa sémantique. Notre résultat principal dans cette direction est la caractérisation des modèles de cette théorie des types, en extrayant une définition mathématique qui leur est équivalente.

We study a type theoretic definition of weak omega-categories originally introduced by Finster and Mimram, inspired both from ideas coming from homotopy type theory and from a definition of weak omega-category due to Grothendieck and Maltsiniotis. The advantages of such an approach are multiple: The language of type theory allows for a definition restricted to only a few rules, it also provides an explicit syntax on which one can perform inductive reasoning, and gives an algorithm for implementing a proof-assistant dedicated to exploring weak omega-categories. The work we present about this type theory is organized along two main axes: We investigate the theoretical grounds for this definition and relate it to an other known definition of weak omega-categories, and we present the proof-assistant based on this theory together with practical considerations to improve its use. We also consider a generalization of this approach to other related higher structures.We start with an introduction to the language of dependent type theory that we rely on to introduce our definitions, presenting both the syntax and the semantics that we study by means of categorical tools. We then present weak omega-categories and a type theory that defines them. We detail the categorical semantics of this theory and our main contribution in this direction establishes an equivalence between its models and the prior definition of weak omega-categories due to Grothendieck and Maltsiniotis. This definition has enabled us to implement a proof-assistant capable of checking whether a given morphism is well-defined in the theory of weak omega-category, and we present this implementation together with a few examples demonstrating both the capabilities of such a tool, and its tediousness in the vanilla version. To improve this issue, we present two main additional features allowing to partially automating its use: The suspension and the functorialization. These two operations are defined by similar techniques of induction on the syntax of the type theory. We then generalize this definition of weak omega-categories and present a type theoretic framework that is both modular enough to allow for defining higher structures, and constrained enough to precisely understand its semantics. This enables us to sketch a connection with the theory of monads with arities. Using this framework, we introduce and study two other definitions of higher structures: Monoidal weak omega-categories and cubical weak omega-categories. By using syntactic reasoning we are able to defines translations back and forth between the type theory defining weak omega-categories and the one describing monoidal weak omega-categories. One of our main result is to show that these translations imply an equivalence at the level of models: It shows that the monoidal omega-categories are equivalent to the omega-categories with a single object thus justifying the correctness of the appellation monoidal. We then give an alternate presentation of the type theory defining monoidal weak omega-categories, which diverges from our framework but is more standalone, and prove it to be equivalent to the previous presentation. We finally introduce in our framework a definition of cubical weak omega-categories and study its semantics, our main result along these lines is to characterize the models of this type theory and extract a mathematical definition equivalent to them., Nous présentons une définition des omega-catégories faibles formulée en théorie des types proposée initialement par Finster et Mimram, suivant des idées provenant à la fois de la théorie homotopique des types et d’une définition des omega-catégories faibles due à Grothendieck et Maltsiniotis. Les avantages d’une telle approche sont multiples : Le langage de la théorie des types permet une définition qui se réduit à quelques règles seulement, et il fournit une syntaxe explicite sur laquelle il est possible de raisonner par induction. Cela donne également un algorithme pour implémenter un assistant de preuve dédié à l’exploration des omega-catégories faibles. Le travail que nous présentons est organisé selon deux axes principaux : Nous étudions les fondements théoriques de cette définition et la relions aux autres définitions connues de omega-catégories faibles, et nous présentons l’assistant de preuve basé sur cette théorie avec des considérations pour rendre cet outil plus utilisable en pratique. Nous considérons également des généralisations de cette approche à d’autres structures supérieures similaires.Nous commençons par présenter une introduction à la théorie des types dépendants sur laquelle repose les définitions que nous étudions, en introduisant à la fois une syntaxe et sa sémantique catégorique. Nous présentons ensuite les omega-catégories faibles avec une théorie des types pour les définir. Nous détaillons la sémantique catégorique de cette théorie et notre contribution principale dans cette direction établit une équivalence entre les modèles de cette théorie et la définition antérieure des omega-catégories faibles due à Grothendieck et Maltsiniotis. Cette définition nous a permis d’implémenter un assistant de preuves capable de vérifier si un morphisme donné est correctement défini dans la théorie des omega-catégories faibles; nous présentons cette implémentation accompagnée de quelques exemples illustrant à la fois les possibilités de l’outil, et l’impraticabilité de son utilisation dans sa version native. Pour corriger ce problème, nous présentons deux fonctionnalités additionnelles permettant une automatisation partielle : La suspension et la fonctorialisation. Ces deux opérations sont définies par des techniques similaires, par induction sur la syntaxe de la théorie des types. Nous généralisons ensuite cette définition des omega-catégories faibles et présentons un cadre pour étudier des théories des types, qui est à la fois suffisamment modulaire pour permettre de définir d’autres structures supérieures, et suffisamment contraint pour étudier précisément sa sémantique. Cela nous permet d’esquisser une connexion avec la théorie des monades à arités. En se reposant sur ce cadre, nous introduisons et étudions deux autres définitions de structures supérieures : les omega-catégories faibles monoidales et les omega-catégories faibles cubiques. Par un raisonnement syntaxique, nous définissons des traductions dans les deux sens entre les théories des types qui définissent les omega-catégories faibles et les omega-catégories faibles monoidales. L’un de nos résultats principaux est de montrer que ces traductions induisent une équivalence au niveau des modèles, montrant que les omega-catégories faibles monoidales sont équivalentes aux omega-catégories qui ont un unique objet justifiant l’appellation de monoidal. Nous donnons ensuite une présentation alternative de la théorie des types pour définir les omega-catégories faibles monoidales, qui diverge de notre cadre, mais qui est plus indépendante, et la prouvons équivalente à la présentation précédente. Finalement nous introduisons dans notre cadre une définition de la théorie des omega-catégories faibles cubiques, et étudions sa sémantique. Notre résultat principal dans cette direction est la caractérisation des modèles de cette théorie des types, en extrayant une définition mathématique qui leur est équivalente.

The subject of this thesis is about lambda-calculus decorated with types, usually called "Church-style typed lambda-calculus". We study this lambda-calculus enhanced with Intersection types, as described by Barendregt, Dekkers and Statman in the book "Lambda-calculus with Types"; Union types, as introduced by Plotkin, MacQueen and Sethi; and Dependent types, as described by Plotkin, Harper and Honsell when they introduced the Edinburgh Logical Framework LF. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the "proof-as-lambda-terms / formulas-as-types" Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. Combining these three type disciplines gives rise to a family of calculi that can be parametrized and classified: we call the resulting system the Delta-calculus. We then discuss the design decisions which have led us to the formulation of these calculi, study their metatheory, and provide various examples of applications; and we finally present a software implementation of the Delta-calculus, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants.; Le sujet de cette thèse est sur le lambda-calcul décoré avec des types, communément appelé « lambda-calcul typé à la Church ». Nous étudions des versions de ce lambda-calcul muni de types intersections, tels que ceux décrits dans le livre « Lambda-calculus with types » de Barendregt, Dekkers et Statman ; les types unions, qui ont été introduits par Plotkin, MacQueen et Sethi ; et les types dépendants, tels qu'ils ont été décrits par Plotkin, Harper et Honsell lorsqu'ils ont introduit le Logical Framework d'Edinbourgh LF. Les types intersections et unions sont un moyen d'exprimer du polymorphisme ad hoc et sont une alternative au polymorphisme paramétrique de Girard. Les types dépendants ont été introduits pour formaliser la logique intuitionniste avec la correspondance de Curry-Howard. Le système de types obtenu peut être enrichi avec une relation de soutypage décidable. La combinaison de ces trois disciplines de type donne lieu à une famille de calculs qui peuvent être paramétrés et classifiés. Nous appelons le système générique le Delta-calcul. Nous discutons ensuite des décisions de conception qui nous ont amené à la formulation de ces calculs, nous étudions leur métathéorie, et nous présentons divers exemples d'applications avant de présenter une implémentation logicielle du Delta-calcul, avec une description des algorithmes de vérification de type, de raffinement, de soutypage, d'évaluation, ainsi que de l'interface en ligne de commande. Ce travail de recherche peut être vu comme un petit pas franchi dans la direction d'une théorie des types alternative pour définir du polymorphisme dans les langages de programmation et dans les assistants de preuve interactifs.

The subject of this thesis is about lambda-calculus decorated with types, usually called "Church-style typed lambda-calculus". We study this lambda-calculus enhanced with Intersection types, as described by Barendregt, Dekkers and Statman in the book "Lambda-calculus with Types"; Union types, as introduced by Plotkin, MacQueen and Sethi; and Dependent types, as described by Plotkin, Harper and Honsell when they introduced the Edinburgh Logical Framework LF. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the "proof-as-lambda-terms / formulas-as-types" Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. Combining these three type disciplines gives rise to a family of calculi that can be parametrized and classified: we call the resulting system the Delta-calculus. We then discuss the design decisions which have led us to the formulation of these calculi, study their metatheory, and provide various examples of applications; and we finally present a software implementation of the Delta-calculus, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants.; Le sujet de cette thèse est sur le lambda-calcul décoré avec des types, communément appelé « lambda-calcul typé à la Church ». Nous étudions des versions de ce lambda-calcul muni de types intersections, tels que ceux décrits dans le livre « Lambda-calculus with types » de Barendregt, Dekkers et Statman ; les types unions, qui ont été introduits par Plotkin, MacQueen et Sethi ; et les types dépendants, tels qu'ils ont été décrits par Plotkin, Harper et Honsell lorsqu'ils ont introduit le Logical Framework d'Edinbourgh LF. Les types intersections et unions sont un moyen d'exprimer du polymorphisme ad hoc et sont une alternative au polymorphisme paramétrique de Girard. Les types dépendants ont été introduits pour formaliser la logique intuitionniste avec la correspondance de Curry-Howard. Le système de types obtenu peut être enrichi avec une relation de soutypage décidable. La combinaison de ces trois disciplines de type donne lieu à une famille de calculs qui peuvent être paramétrés et classifiés. Nous appelons le système générique le Delta-calcul. Nous discutons ensuite des décisions de conception qui nous ont amené à la formulation de ces calculs, nous étudions leur métathéorie, et nous présentons divers exemples d'applications avant de présenter une implémentation logicielle du Delta-calcul, avec une description des algorithmes de vérification de type, de raffinement, de soutypage, d'évaluation, ainsi que de l'interface en ligne de commande. Ce travail de recherche peut être vu comme un petit pas franchi dans la direction d'une théorie des types alternative pour définir du polymorphisme dans les langages de programmation et dans les assistants de preuve interactifs.

This thesis is about the metatheory of intuitionnistic type theory. The considered systems are variants of Martin-Löf type theory of Calculus of Constructions, and we are interested in the coherence of those systems and in the independence of axioms with respect to those systems. The common theme of this thesis is the construction of syntactic models, which are models reusing type theory to interpret type theory. In a first part, we introduce type theory by a minimal system and several possible extensions. In a second part, we introduce the syntactic models given by program translation and give several examples. In a third part, we present Template-Coq, a plugin for metaprogramming in Coq. We demonstrate how to use it to implement directly some syntactic models. Last, we consider type theories with two equalities: one strict and one univalent. We propose a re-reading of works of Coquand et.al. and of Orton and Pitts on the cubical model by introducing degenerate fibrancy.; Cette thèse s'intéresse à la métathéorie de la théorie des types intuitionniste. Les systèmes que nous considérons sont des variantes de la théorie des types de Martin-Löf ou du Calcul des Constructions, et nous nous intéressons à la cohérence de ces systèmes ou encore à l'indépendance d'axiomes par rapport à ces systèmes. Le fil rouge de cette thèse est la construction de modèles syntaxiques, qui sont des modèles qui réutilisent la théorie des types pour interpréter la théorie des types. Dans une première partie, nous introduisons la théorie des types à l'aide d'un système minimal et de plusieurs extensions potentielles. Dans une seconde partie, nous introduisons les modèles syntaxiques donnés par traduction de programme et donnons plusieurs exemples. Dans une troisième partie, nous présentons Template-Coq, un plugin de métaprogrammation pour Coq. Nous montrons comment l'utiliser pour implémenter directement certains modèles syntaxiques. Enfin, dans une dernière partie, nous nous intéressons aux théories des types à deux égalités : une égalité stricte et une égalité univalente. Nous proposons une relecture des travaux de Coquand et. al. et Orton et Pitts sur le modèle cubique en introduisant la notion de fibrance dégénérée.

This thesis is about the metatheory of intuitionnistic type theory. The considered systems are variants of Martin-Löf type theory of Calculus of Constructions, and we are interested in the coherence of those systems and in the independence of axioms with respect to those systems. The common theme of this thesis is the construction of syntactic models, which are models reusing type theory to interpret type theory. In a first part, we introduce type theory by a minimal system and several possible extensions. In a second part, we introduce the syntactic models given by program translation and give several examples. In a third part, we present Template-Coq, a plugin for metaprogramming in Coq. We demonstrate how to use it to implement directly some syntactic models. Last, we consider type theories with two equalities: one strict and one univalent. We propose a re-reading of works of Coquand et.al. and of Orton and Pitts on the cubical model by introducing degenerate fibrancy.; Cette thèse s'intéresse à la métathéorie de la théorie des types intuitionniste. Les systèmes que nous considérons sont des variantes de la théorie des types de Martin-Löf ou du Calcul des Constructions, et nous nous intéressons à la cohérence de ces systèmes ou encore à l'indépendance d'axiomes par rapport à ces systèmes. Le fil rouge de cette thèse est la construction de modèles syntaxiques, qui sont des modèles qui réutilisent la théorie des types pour interpréter la théorie des types. Dans une première partie, nous introduisons la théorie des types à l'aide d'un système minimal et de plusieurs extensions potentielles. Dans une seconde partie, nous introduisons les modèles syntaxiques donnés par traduction de programme et donnons plusieurs exemples. Dans une troisième partie, nous présentons Template-Coq, un plugin de métaprogrammation pour Coq. Nous montrons comment l'utiliser pour implémenter directement certains modèles syntaxiques. Enfin, dans une dernière partie, nous nous intéressons aux théories des types à deux égalités : une égalité stricte et une égalité univalente. Nous proposons une relecture des travaux de Coquand et. al. et Orton et Pitts sur le modèle cubique en introduisant la notion de fibrance dégénérée.

The type system of higher-order logic allows to exclude some unexpected expressions such as the application of a predicate to itself. However, it is not sufficient to verify more complex criteria such as the absence of divisions by zero. This thesis is dedicated to the study of an extension of higher-order logic, named predicate subtyping, whose purpose is to make the assignment of types as expressive as the assignment of predicates. Starting from a type A and a predicate P(x) of domain A, predicate subtyping allows to build a subtype of A, denoted {x : A | P(x)}, whose elements are the terms t of type A such that P(t) is provable. Predicate subtyping is at the heart of the proof system PVS.This work presents the formalization of a minimal system expressing predicate subtyping, named PVS-Core, as well as a system of verifiable certificates for PVS-Core. This second system, named PVS-Cert, is based on the introduction of proof terms and explicit coercions. PVS-Core and PVS-Cert are equipped with a notion of conversion corresponding respectively to equality modulo beta and to equality modulo beta and the erasure of coercions, chosen to establish a simple correspondence between the two systems.The construction of PVS-Cert is similar to that of PTSs (Pure Type Systems) with dependent pairs and PVS-Cert can be equipped with the notion of beta-sigma-reduction used at the core of these systems. One of the main theorems proved in this work is the strong normalization of both the reduction underlying the conversion and beta-sigma-reduction. This theorem allows, on the one hand, to build a type-checking (and proof-checking) algorithm for PVS-Cert and, on the other hand, to prove a cut elimination result, used in turn to prove important properties of the two studied systems. Furthermore, it is also proved that PVS-Cert is a conservative extension of the PTS lambda-HOL and that, as a consequence, PVS-Core is a conservative extension of higher-order logic.A second part presents the prototype of an instrumentation of PVS to generate proof certificates. A third and final part is dedicated to the study of links between classical and constructive logic, with the definition of a minimal double-negation translation as well as the presentation of an automated proof constructivization algorithm.; Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit pas pour vérifier des critères plus complexes comme l'absence de divisions par zéro. Cette thèse est consacrée à l’étude d’une extension de la logique d’ordre supérieur appelée sous-typage par prédicats (predicate subtyping), dont l'objet est de rendre l'attribution de types aussi expressive que l'attribution de prédicats. A partir d'un type A et d'un prédicat P(x) de domaine A, le sous-typage par prédicats permet de construire un sous-type de A, noté {x : A | P(x)}, dont les éléments sont les termes t de type A tels que P(t) est démontrable. Le sous-typage par prédicats est au coeur du système PVS. Ce travail présente la formalisation d'un système minimal incluant le sous-typage par prédicats, appelé PVS-Core, ainsi qu'un système de certificats vérifiables pour PVS-Core. Ce deuxième système, appelé PVS-Cert, repose sur l'introduction de termes de preuves et de coercions explicites. PVS-Core et PVS-Cert sont munis d'une notion de conversion correspondant respectivement à l'égalité modulo beta et à l'égalité modulo beta et effacement des coercions, choisi pour établir une correspondance simple entre les deux systèmes. La construction de PVS-Cert est semblable à celle des PTS (Pure Type Systems) avec paires dépendantes et PVS-Cert peut être muni de la notion de beta-sigma-réduction utilisée au coeur de ces systèmes. L'un des principaux théorèmes démontré dans ce travail est la normalisation forte de la réduction sous-jacente à la conversion et de la beta-sigma-réduction. Ce théorème permet d'une part de construire un algorithme de vérification du typage (et des preuves) pour PVS-Cert et d'autre part de démontrer un résultat d'élimination des coupures, utilisé à son tour pour prouver plusieurs propriétés importantes des deux systèmes étudiés. Par ailleurs, il est également démontré que PVS-Cert est une extension conservative du PTS lambda-HOL, et qu'en conséquence PVS-Core est une extension conservative de la logique d'ordre supérieur. Une deuxième partie présente le prototype d'une instrumentation de PVS pour produire des certificats de preuve. Une troisième et dernière partie est consacrée à l'étude de liens entre logique classique et constructive avec la définition d'une traduction par double négation minimale ainsi que la présentation d'un algorithme de constructivisation automatique des preuves.

The type system of higher-order logic allows to exclude some unexpected expressions such as the application of a predicate to itself. However, it is not sufficient to verify more complex criteria such as the absence of divisions by zero. This thesis is dedicated to the study of an extension of higher-order logic, named predicate subtyping, whose purpose is to make the assignment of types as expressive as the assignment of predicates. Starting from a type A and a predicate P(x) of domain A, predicate subtyping allows to build a subtype of A, denoted {x : A | P(x)}, whose elements are the terms t of type A such that P(t) is provable. Predicate subtyping is at the heart of the proof system PVS.This work presents the formalization of a minimal system expressing predicate subtyping, named PVS-Core, as well as a system of verifiable certificates for PVS-Core. This second system, named PVS-Cert, is based on the introduction of proof terms and explicit coercions. PVS-Core and PVS-Cert are equipped with a notion of conversion corresponding respectively to equality modulo beta and to equality modulo beta and the erasure of coercions, chosen to establish a simple correspondence between the two systems.The construction of PVS-Cert is similar to that of PTSs (Pure Type Systems) with dependent pairs and PVS-Cert can be equipped with the notion of beta-sigma-reduction used at the core of these systems. One of the main theorems proved in this work is the strong normalization of both the reduction underlying the conversion and beta-sigma-reduction. This theorem allows, on the one hand, to build a type-checking (and proof-checking) algorithm for PVS-Cert and, on the other hand, to prove a cut elimination result, used in turn to prove important properties of the two studied systems. Furthermore, it is also proved that PVS-Cert is a conservative extension of the PTS lambda-HOL and that, as a consequence, PVS-Core is a conservative extension of higher-order logic.A second part presents the prototype of an instrumentation of PVS to generate proof certificates. A third and final part is dedicated to the study of links between classical and constructive logic, with the definition of a minimal double-negation translation as well as the presentation of an automated proof constructivization algorithm.; Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit pas pour vérifier des critères plus complexes comme l'absence de divisions par zéro. Cette thèse est consacrée à l’étude d’une extension de la logique d’ordre supérieur appelée sous-typage par prédicats (predicate subtyping), dont l'objet est de rendre l'attribution de types aussi expressive que l'attribution de prédicats. A partir d'un type A et d'un prédicat P(x) de domaine A, le sous-typage par prédicats permet de construire un sous-type de A, noté {x : A | P(x)}, dont les éléments sont les termes t de type A tels que P(t) est démontrable. Le sous-typage par prédicats est au coeur du système PVS. Ce travail présente la formalisation d'un système minimal incluant le sous-typage par prédicats, appelé PVS-Core, ainsi qu'un système de certificats vérifiables pour PVS-Core. Ce deuxième système, appelé PVS-Cert, repose sur l'introduction de termes de preuves et de coercions explicites. PVS-Core et PVS-Cert sont munis d'une notion de conversion correspondant respectivement à l'égalité modulo beta et à l'égalité modulo beta et effacement des coercions, choisi pour établir une correspondance simple entre les deux systèmes. La construction de PVS-Cert est semblable à celle des PTS (Pure Type Systems) avec paires dépendantes et PVS-Cert peut être muni de la notion de beta-sigma-réduction utilisée au coeur de ces systèmes. L'un des principaux théorèmes démontré dans ce travail est la normalisation forte de la réduction sous-jacente à la conversion et de la beta-sigma-réduction. Ce théorème permet d'une part de construire un algorithme de vérification du typage (et des preuves) pour PVS-Cert et d'autre part de démontrer un résultat d'élimination des coupures, utilisé à son tour pour prouver plusieurs propriétés importantes des deux systèmes étudiés. Par ailleurs, il est également démontré que PVS-Cert est une extension conservative du PTS lambda-HOL, et qu'en conséquence PVS-Core est une extension conservative de la logique d'ordre supérieur. Une deuxième partie présente le prototype d'une instrumentation de PVS pour produire des certificats de preuve. Une troisième et dernière partie est consacrée à l'étude de liens entre logique classique et constructive avec la définition d'une traduction par double négation minimale ainsi que la présentation d'un algorithme de constructivisation automatique des preuves.

International audience

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

L'appréhension de la complexité logique en mathématique offre unelongue tradition de mise en place de modèles pour des logiquescomplexes obtenus par extension de modèles pour des logiques plussimples, comme c'est le cas pour la construction de faisceaux. Eninformatique, cette démarche a un pendant dual qui consiste à donnerdu sens à des langages complexes via une phase de compilation vers deslangages plus simples.Dans ce manuscrit, nous montrons en quoi l'approche par compilationfait aussi sens en logique, via l'isomorphisme de Curry-Howard, et esten fait plus précise que l'approche par extension de modèle car elleprend en compte le calcul. Pour illustrer ce propos, nous donnons desexemples de transformation de programmes en théorie des types, avecune application à l'assistant de preuve Coq, et dans une moindremesure en programmation distribuée.

Dedukti is a Logical Framework resulting from the combination ofdependent typing and rewriting. It can be used to encode many logicalsystems using shallow embeddings preserving their notion of reduction.These translations of logical systems in a common format are anecessary first step for exchanging proofs between systems. Thisobjective of interoperability of proof systems is the main motivationof this thesis.To achieve it, we take inspiration from the world of programminglanguages and more specifically from object-oriented languages becausethey feature advanced mechanisms for encapsulation, modularity, anddefault definitions. For this reason we start by a shallowtranslation of an object calculus to Dedukti. The most interestingpoint in this translation is the treatment of subtyping.Unfortunately, it seems very hard to incorporate logic in this objectcalculus. To proceed, object-oriented mechanisms should be restrictedto static ones which seem enough for interoperability. Such acombination of static object-oriented mechanisms and logic is alreadypresent in the FoCaLiZe environment so we propose a shallow embeddingof FoCaLiZe in Dedukti. The main difficulties arise from theintegration of FoCaLiZe automatic theorem prover Zenon and from thetranslation of FoCaLiZe functional implementation language featuringtwo constructs which have no simple counterparts in Dedukti: localpattern matching and recursion.We then demonstrate how this embedding of FoCaLiZe to Dedukti can beused in practice for achieving interoperability of proof systemsthrough FoCaLiZe, Zenon, and Dedukti. In order to avoid strengtheningto much the theory in which the final proof is expressed, we useDedukti as a meta-language for eliminating unnecessary axioms., Dedukti est un cadre logique résultant de la combinaison du typagedépendant et de la réécriture. Il permet d'encoder de nombreuxsystèmes logiques au moyen de plongements superficiels qui préserventla notion de réduction.Ces traductions de systèmes logiques dans un format commun sont unepremière étape nécessaire à l'échange de preuves entre cessystèmes. Cet objectif d'interopérabilité des systèmes de preuve estla motivation principale de cette thèse.Pour y parvenir, nous nous inspirons du monde des langages deprogrammation et plus particulièrement des langages orientés-objetparce qu'ils mettent en œuvre des mécanismes avancés d'encapsulation,de modularité et de définitions par défaut. Pour cette raison, nouscommençons par une traduction superficielle d'un calcul orienté-objeten Dedukti. L'aspect le plus intéressant de cette traduction est letraitement du sous-typage.Malheureusement, ce calcul orienté-objet ne semble pas adapté àl'incorporation de traits logiques. Afin de continuer, nous devonsrestreindre les mécanismes orientés-objet à des mécanismes statiques,plus faciles à combiner avec la logique et apparemment suffisant pournotre objectif d'interopérabilité. Une telle combinaison de mécanismesorientés-objet et de logique est présente dans l'environnementFoCaLiZe donc nous proposons un encodage superficiel de FoCaLiZe dansDedukti. Les difficultés principales proviennent de l'intégration deZenon, le prouveur automatique de théorèmes sur lequel FoCaLiZerepose, et de la traduction du langage d'implantation fonctionnel deFoCaLiZe qui présente deux constructions qui n'ont pas decorrespondance simple en Dedukti : le filtrage de motif local et larécursivité.Nous démontrons finalement comment notre encodage de FoCaLiZe dansDedukti peut servir en pratique à l'interopérabilité entre dessystèmes de preuve à l'aide de FoCaLiZe, Zenon et Dedukti. Pour éviterde trop renforcer la théorie dans laquelle la preuve finale estobtenue, nous proposons d'utiliser Dedukti en tant que méta-langagepour éliminer des axiomes superflus.

The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3; L’objectif de cette thèse est de démontrer que π4(S3) ≃ Z/2Z en théorie des types homotopiques. En particulier, c’est une démonstration constructive et purement homotopique. On commence par rappeler les concepts de base de la théorie des types homotopiques et on démontre quelques résultats bien connus sur les groupes d’homotopie des sphères : le calcul des groupes d’homotopie du cercle, le fait que ceux de la forme πk(Sn) avec k < n sont triviaux et la construction de la fibration de Hopf. On passe ensuite à des outils plus avancés. En particulier, on définit la construction de James, ce qui nous permetde démontrer le théorème de suspension de Freudenthal et le fait qu’il existe un entier naturel n tel que π4(S3) ≃ Z/2Z. On étudie ensuite le produit smash des sphères, on construit l’anneau de cohomologie des espaces et on introduit l’invariant de Hopf, ce qui nous permet de montrer que n est égal soit à 1, soit à 2. L’invariant de Hopf nous permet également de montrer que tous les groupes de la forme π4n−1(S2n) sont infinis. Finalement, on construit la suite exacte de Gysin, ce qui nous permet de calculer la cohomologie de CP2 et de démontrer que π4(S3) ≃ Z/2Z, et que plus généralement on a πn+1(Sn) ≃ Z/2Z pour tout n ≥ 3

Sheafification is a popular tool in topos theory which allows to extend the internal logic of a topos with new principles. One of its most famous applications is the possibility to transform a topos into a boolean topos using the dense topology, which corresponds in essence to Gödel’s double negation translation. The same construction has not been developed in Martin-Löf type theory because of a mismatch between topos theory and type theory. This mismatched has been fixed recently by considering homotopy type theory, an extension of Martin-Löf type theory with new principles inspired by category theory and homotopy theory, and which corresponds closely to higher toposes. In this paper, we give a computer-checked construction of Lawvere-Tierney sheafification in homotopy type theory., Journal of Formalized Reasoning, Vol 9, No 2 (2016)

Version soutenance; This thesis presents a programming language for developingpurely computational certified programs.We present two type systems. The first one, ICC_Σ, extends Miquel'sImplicit Calculus of Constructions (ICC) with dependent sums. ICC_Σ isa Curry-style system with implicit type operators. With theseoperators, logical information may remain implicit, which makes itpossible to write purely computational certified programs. Addingdependent sums gives more expressive power to the system and is afirst step towards adding inductive types that are already built-inthe Coq proof assistant. One drawback of ICC_Σ is that type inferenceis likely to be undecidable. To solve that issue, we define a second system : the AnnotatedImplicit Calculus of Constructions, AICC_Σ. AICC_Σ is a type systemequivalent to ICC_Σ but with a bicolor Church-style syntax. Logicalinformation may appear explicitly, thus making type inferencedecidable. A built-in erasure procedure, that removes recursively theflagged parts, transforms an annotated AICC_Σ term into a purelycomputational ICC_Σ term. We prove that this procedure is correct andcomplete, which implies that valid AICC_Σ programs correspond exactlyto valid ICC_Σ ones. We also define a correct and complete type inference algorithm forAICC_Σ. This algorithm, combined with the erasure procedure makescertified programming in ICC_Σ possible.; Cette thèse propose un langage permettant de développer des programmescertifiés purement calculatoires. Pour cela deux systèmes de types sont présentés. Le premier, ICC_Σ,est une extension du Calcul des Constructions Implicite de Miquel(ICC), enrichi avec des sommes dépendantes. ICC_Σ est un système à laCurry avec des opérateurs de type implicite. Ces opérateurs permettentaux indications logiques de ne pas apparaître explicitement dans lestermes, rendant possible l'écriture de programmes certifiés purementcalculatoires. L'ajout des sommes dépendantes donne plusd'expressivité au système et est un premier pas en vue de l'ajout destypes inductifs, déjà présents dans l'assistant de preuves Coq. Unelimitation de ICC_Σ est que l'inférence de type est vraisemblablementindécidable. Pour contourner ce problème, nous définisssons un deuxième système:le Calcul des Constructions Implicite Annoté avec sommes dépendantes,noté AICC_Σ. AICC_Σ est un système de types équivalent à ICC_Σ, maisavec une syntaxe bicolore à la Church. Les indications logiques desprogrammes apparaissent explicitement, rendant l'inférence de typedécidable, mais peuvent être marquées. AICC_Σ est muni d'un mécanismeinterne d'effacement qui transforme un terme de AICC_Σ avecindications logiques en un terme de ICC_Σ purement calculatoire. Nousprouvons que cet effacement est correct et complet, ce qui signifieque les programmes valides de AICC_Σ correspondent exactement à ceuxde ICC_Σ. Nous définissons également un algorithme d'inférence de type correctet complet pour AICC_Σ. La combinaison de cet algorithme et dumécanisme d'effacement rend possible la programmation certifiée dansICC_Σ.

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.; 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é.

The concept of liquid clocks introduced in this paper is a significant step towards a more precise compile-time framework for the analysis of synchronous and polychromous languages. Compiling languages such as Lustre or Signal indeed involves a number of static analyses of programs before they can be synthesized into executable code, e.g., synchronicity class characterization, clock assignment, static scheduling or causality analysis. These analyses are often equivalent to undecidable problems, necessitating abstracting such programs to provide sound yet incomplete analyses. Such abstractions unfortunately often lead to the rejection of programs that could very well be synthesized into deterministic code, provided abstraction refinement steps could be applied for more accurate analysis. To reduce the number of false negatives occurring during the compilation process, we leverage recent advances in type theory — with the definition of decidable classes of value-dependent type systems — and formal verification, linked to the development of efficient SAT/SMT solvers, to provide a type-theoretic approach that considers all the above analyses as type inference problems. To simplify the exposition of our new approach in this paper, we define a refinement type system for a minimalistic, synchronous, stream-processing language to concisely represent, analyze, and verify logical and quantitative properties of programs expressed as stream-processing data-flow networks. Our type system provides a new framework for representing logical time (clocks) and scheduling properties, and to describe their relations with stream values and, possibly, other quantas. We show how to analyze synchronous stream processing programs (a la Lustre, Signal) to enable previously described analyses involved in compiling such programs. We also prove the soundness of our type system and elaborate on the adaptability of this core framework by outlining its extensibility to specific models of computations and other quantas.

This thesis focuses on two problems on l-modular representation theory of p-adic groups. Let F be a non-archimedean local field of residue characteristic p different from l. In the first part, we study block decomposition of the category of smooth modular representations of GL(n; F) and its inner forms.We want to reduce the description of a positive-level block 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 of category theory, we reduce the problem to find an isomorphism between two intertwining algebras. The proof of the existence of such an isomorphism is not complete because it relies on a conjecture that we state and we prove for several cases. In the second part we generalize the construction of metaplectic group and Weil representation in the case of representations over un integral domain. We define a central extension of the symplectic group over F by the multiplicative group of an integral domain. We prove that it satisfies the same properties as in the complex case. Cette thèse traite deux problèmes concernant la théorie des représentations l-modulaires d’un groupe p-adique. Soit F un corps local non archimédien de caractéristique résiduelle p différente de l. Dans la première partie, on étudie la décomposition en blocs de la catégorie des représentations lisses `-modulaires de GL(n; F) et de ses formes intérieures. On veut ramener la description d’un bloc de niveau positif à celle d’un bloc de niveau 0 (d’un autre groupe du même type) en cherchant des équivalences de catégories. En utilisant la théorie des types de Bushnell-Kutzko dans le cas modulaire et un théorème de la théorie des caté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 une conjecture qu’on énonce et qui est prouvée pour plusieurs cas. Dans une deuxième partie on généralise la construction du groupe métaplectique et de la représentation de Weil dans le cas des représentations sur un anneau intègre. On construit une extension centrale du groupe symplectique sur F par le groupe multiplicatif d’un anneau intègre et on prouve qu’il satisfait les mêmes propriétés que dans le cas des représentations complexes.

Partant de son travail Mathematics of Infinity (1989), Martin-Löf a développé l'idée d'un lien conceptuel profond entre les notions de suite de choix et d'objet mathématique nonstandard. Précisément, il a défini une extension nonstandard de la théorie des types en ajoutant une série d'axiomes nonstandard conçue comme une sorte de suite de choix. Enfin, dans une communication de 1999, il a présenté les grandes lignes d'une théorie des types nonstandard plus générale et munie d'un fort contenu computationnel. Le présent travail est une tentative de donner un développement complet d'une théorie de ce genre. Cependant, dans le but de garder un fort contrôle sur la théorie résultante et notablement pour éviter quelques problèmes en rapport avec l'égalité définitionnelle, le champ des axiomes nonstandard est moins général que ceux proposés dans sa communication de 1999. L'étude présente est poussée jusqu'à l' introduction d'une notion de proposition externe qui joue le même rôle que les propriétés externes si utiles dans l'analyse nonstandard usuelle. Du fait que ce texte débute par une introduction à la théorie des types de Martin-Löf, il peut intéresser les mathématiciens non familiers avec ce sujet.

Making sure that a computer program behaves as expected, especially in critical applications (health, transport, energy, communications, etc.), is more and more important, all the more so since computer programs become more and more ubiquitous and essential to the functioning of modern societies. But how to check that a program behaves as expected, in particular when the range of its inputs is very large or potentially infinite? In this work, we explain the development of a new, faster and formally proved version of Rainbow based on the extraction mechanism of Coq. The previous version of Rainbow verified a CPF le in two steps. First, it used a non-certified OCaml program to translate a CPF file into a Coq script, using the Coq libraries on rewriting theory and termination CoLoR and Coccinelle. Second, it called Coq to check the correctness of the script. This approach is interesting for it provides a way to reuse in Coq termination proofs generated by external tools. This is also the approach followed by CiME3. However, it suffers from a number of deficiencies. First, because in Coq functions are interpreted, computation is much slower than with programs written in a standard programming language and compiled into binary code. Second, because the translation from CPF to Coq is not certified, it may contain errors and either lead to the rejection of valid certificates, or to the acceptance of wrong certificates. To solve the latter problem, one needs to define and formally prove the correctness of a function checking whether a certificate is valid or not. To solve the former problem, one needs to compile this function to binary code. The present work shows how to solve these two problems by using the proof assistant Coq and its extraction mechanism to the programming language OCaml. Indeed, data structures and functions de fined in Coq can be translated to OCaml and then compiled to binary code by using the OCaml compiler. A similar approach was first initiated in CeTA using the Isabelle proof assistant., S'assurer qu'un programme informatique se comporte bien, surtout dans des applications critiques (santé, transport, énergie, communications, etc.) est de plus en plus important car les ordinateurs et programmes informatiques sont de plus en plus omniprésents, voir essentiel au bon fonctionnement de la société. Mais comment vérifier qu'un programme se comporte comme prévu, quand les informations qu'il prend en entrée sont de très grande taille, voire de taille non bornée a priori ? Pour exprimer avec exactitude ce qu'est le comportement d'un programme, il est d'abord nécessaire d'utiliser un langage logique formel. Cependant, comme l'a montré Gödel dans, dans tout système formel suffisamment riche pour faire de l'arithmétique, il y a des formules valides qui ne peuvent pas être prouvées. Donc il n'y a pas de programme qui puisse décider si toute propriété est vraie ou fausse. Cependant, il est possible d'écrire un programme qui puisse vérifier la correction d'une preuve. Ce travail utilisera justement un tel programme, Coq, pour formellement vérifier la correction d'un certain programme. Dans cette thèse, nous expliquons le développement d'une nouvelle version de Rainbow, plus rapide et plus sûre, basée sur le mécanisme d'extraction de Coq. La version précédente de Rainbow vérifiait un certificat en deux étapes. Premièrement, elle utilisait un programme OCaml non certifié pour traduire un fichier CPF en un script Coq, en utilisant la bibliothèque Coq sur la théorie de la réécriture et la terminaison appelée CoLoR. Deuxièmement, elle appelait Coq pour vérifier la correction du script ainsi généré. Cette approche est intéressante car elle fournit un moyen de réutiliser dans Coq des preuves de terminaison générée par des outils extérieurs à Coq. C'est également l'approche suivie par CiME3. Mais cette approche a aussi plusieurs désavantages. Premièrement, comme dans Coq les fonctions sont interprétées, les calculs sont beaucoup plus lents qu'avec un langage où les programmes sont compilés vers du code binaire exécutable. Deuxièmement, la traduction de CPF dans Coq peut être erronée et conduire au rejet de certificats valides ou à l'acceptation de certificats invalides. Pour résoudre ce deuxième problème, il est nécessaire de définir et prouver formellement la correction de la fonction vérifiant si un certificat est valide ou non. Et pour résoudre le premier problème, il est nécessaire de compiler cette fonction vers du code binaire exécutable. Cette thèse montre comment résoudre ces deux problèmes en utilisant l'assistant à la preuve Coq et son mécanisme d'extraction vers le langage de programmation OCaml. En effet, les structures de données et fonctions définies dans Coq peuvent être traduits dans OCaml et compilées en code binaire exécutable par le compilateur OCaml. Une approche similaire est suivie par CeTA en utilisant l'assistant à la preuve Isabelle et le langage Haskell.

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

This thesis studies the cooperation between the Coq proof assistant and external provers through proof witnesses. We concentrate on two different kinds of provers that can return certicates: first, answers coming from SAT and SMT solvers can be checked in Coq to increase both the confidence in these solvers and Coq's automation; second, theorems established in interactive provers based on Higher-Order Logic can be exported to Coq and checked again, in order to offer the possibility to produce formal developments which mix these two dierent logical paradigms. It ended up in two software: SMTCoq, a bi-directional cooperation between Coq and SAT/SMT solvers, and HOLLIGHTCOQ, a tool importing HOL Light theorems into Coq. For both tools, we took great care to define a modular and efficient architecture, based on three clearly separated ingredients: an embedding of the formalism of the external tool inside Coq which is carefully translated into Coq terms, a certified checker to establish the proofs using the certicates, and an Ocaml preprocessor to transform proof witnesses coming from different provers into a generic certificate. This division allows that a change in the format of proof witnesses only affects the preprocessor, but no proved Coq code. Another fundamental component for efficiency and modularity is computational reflection, which exploits the computational power of Coq to establish generic and small proofs based on the certicates.; 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.

This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to build a logic from a programming language, both described as pure type systems. This logic provides formulas to express properties of programs and offers a formal framework that allows us to develop a theory of realizability in which realizers of formulas are exactly programs of the starting programming language. In our framework, the standard representation theorems of Gödel's system T and Girard's system F may be seen as two instances of a more general theorem. Then, we explain how the so-called « logical relations » of parametricity theory may be expressed in terms of realizability, which shows that the generated logic provides an adequate framework for developping a general theory of parametricity. Finally, we show how this parametricity theory can be adapted to the underlying type system of the proof assistant Coq and we give an original example of application of parametricity theory to the formalization of mathematics.; Cette thèse porte sur l’adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d’un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques.

International audience; Cet article décrit les étapes qui composent notre analyse du discours, en partant du texte brut, et pour en produire une représentation sémantique dans le cadre de la Discourse Representation Theory, désormais DRT (Kamp and Reyle, 1993). Une chaîne complète de traitement est proposée et testée sur le corpus Itipy, "Itinéraires Pyrénéens", lequel a été proposé par la médiathèque de Pau. Le premier but applicatif consiste à attacher un lieu aux portions de texte narrant une action dans ce lieu. Nous exploitons alors ce corpus de récits de voyage du XIXème siècle dans l'objectif d'extraire automatiquement les itinéraires décrits et afin d'indexer les portions de texte prenant effectivement pour décors les lieux géographiques en question. Notre outil, Grail est un parser pour grammaire logique de types avec un ensemble restreint de règles fixes et utilisant un lexique riche. Tout d'abord, la première phase a consisté en l'acquisition de la grammaire sur un corpus annoté (Paris 7 Treebank). Ce corpus nous a permis d'obtenir les informations grammaticales propres aux unités du lexique de la langue française présentes dans le corpus, le lexique produit ne contient donc pas la totalité des mots du français et contient plusieurs catégories pour les entrées les plus fréquentes. Dans la chaine de traitement, la méthode d'attribution de la catégorie intègre une approche statistique : lors- qu'un mot est absent du lexique, l'analyse propose une catégorie ou lorsqu'il présente plusieurs catégories possibles, elle sélectionne la plus appropriée. Chaque mot du texte est taggé, puis supertaggé en fonction des autres unités se trouvant dans son contexte proche (la phrase). Le supertagger propose plusieurs formules qui correspondent à une analyse syntaxique partielle pour chaque phrase du texte dans le cadre des grammaires catégorielles, et plus précisément du calcul de Lambek. S'ensuit une étape de combinaison de toutes les analyses partielles pour donner l'analyse globale. La structure obtenant la meilleure probabilité étant sélectionnée, on garde cette structure comme organisation du calcul de la représentation sémantique en fonction des unités qui la composent. On associe alors à chaque mot son λ-terme à partir du lexique sémantique cette fois et dont la formule correspond à celle présente dans le lexique grammatical pour cette même entrée (Moot, 2010). Le λ -terme pour chaque unité sémantique est saisi à la main dans le style de la λ -DRT. La représentation sémantique étant produite automatiquement à partir de l'analyse syntaxique, nous obtenons une représentation logique sémantique bien formée. La dimension pragmatique quant à elle ne peut être reléguée à un plan inférieur dans l'interprétation du discours. En effet, une analyse du discours impose de fait une interaction entre la sémantique des unités de langue dont on doit interpréter le sens en discours et la prise en compte de la dimension pragmatique de ce qui est dit. Notre approche s'inspire de l'approche de Busquets et al. (2001), "une théorie de l'interprétation des discours doit être aussi en fait une théorie de la sémantique, de la pragmatique, et de leur interaction, c'est-à-dire une théorie de l'interface pragmatique-sémantique" . Certains phénomènes sémantiques restent cependant difficiles à traiter, certains cas de glissement de sens montrent qu'une flexibilité dans le typage doit être permise, alors que dans les cas les plus courants le typage doit être rigide pour éviter une repré- sentation inappropriée. Nous donnerons quelques exemples à propos et proposons donc afin d'améliorer les résultats de notre chaîne traitement de traiter ces phénomènes par l'affinement des λ -termes du lexique dans le cadre du système F, λ -calcul d'ordre supérieur. Nous détaillerons ici notre corpus et nos objectifs applicatifs quant à celui-ci, nous présenterons les étapes de traitement du discours, commençant par l'acquisition de la grammaire du français sur corpus annoté, puis l'analyse syntaxique dans le cadre des grammaires catégorielles. Nous expliquerons plus amplement l'interface syntaxe-sémantique dans la théorie des types logiques permettant la construction de nos repré- sentations sémantiques en λ-DRT. Nous présenterons le système F et notre traitement des phénomènes discursifs mettant en jeu l'interaction sémantique-pragmatique puis nous présenterons les perspectives de ce travail.

International audience; Cet article présente notre utilisation de la théorie des types dans laquelle nous nous situons pour l'analyse syntaxique, sémantique et pour la construction du lexique. Notre outil, Grail permet de traiter le discours automatiquement à partir du texte brut et nous le testons sur un corpus de récit de voyages pyrénéens, Ititpy. Nous expliquons donc notre usage des grammaires catégorielles et plus particulièrement du calcul de Lambek et la correspondance entre ces catégories et le λ-calcul simplement typé dans le cadre de la DRT. Une flexibilité du typage doit être autorisée dans certains cas et bloquée dans d'autres. Quelques phénomènes linguistiques participant à une forme de glissement de sens provocant des conflits de types sont présentés. Nous expliquons ensuite nos motivations d'ordre pragmatique à utiliser un système à sortes et types variables en sémantique lexicale puis notre traitement compositionnel du temps des évènements inspiré du Binary Tense de (Verkuyl, 2008).

Pedagogical formal systems have appeared recently for propositional calculus (up to the higher order), and it consists of systematically give examples of introduced notions (hypotheses). Formally, it means that to use a set Delta of formulas as hypotheses, one must first give a substitution sigma such that all the instances of formulas sigma(Delta) can be proved. This neccesity of giving examples has been pointed out by Poincaré (1913) as a common-sense practice: a definition of an object by means of assumptions has interest only if such an object can be constructed. This restriction applied to intuitionistic formal systems is consistent with the idea of negationless mathematics advocated by Griss (1946) in the middle of the past century, and shown as a more deep view of intuitionism. Through the Curry-Howard isomorphism (1980), the computational counterpart is the utility of programs defined in the associated functional systems: every function can be applied to a closed value. First results concerning propositional calculi up to the second-order has recently been published by Colson and Michel (2007, 2008, 2009). In this thesis we present an attempt to standardize and to extend to the Calculus of Constructions (CC) those previous results. First a formal and precise definition of pedagogical sub-systems of the Calculus of Constructions is introduced, and different such sub-systems are exhibited as examples., Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version approfondie de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondants: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans cette thèse une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple.

The Coq proof assistant mechanically checks the consistency of the logical reasoning in a proof. It can also be used to develop certified programs. Indeed, Coq uses internally a typed language derived from λ-calculus, the calculus of inductive constructions (CIC). This language can be directly used by a programmer, and a procedure — extraction — allows one to translate CIC programs into more widely used languages such as OCaml, Haskell or Scheme.Extraction is not a mere syntax change: the type system of CIC is very rich, but purely logical entities can appear inside programs, impacting their performance. Extraction erases these logical artefacts as well.In this thesis, we tackle certification of the extraction itself. We have proved its correction in the context of a full formalization of Coq in Coq. Even though this formalization is not exactly Coq, we worked on it with the concrete implementation of Coq in mind. We also propose a new way to certify extracted programs, in the concrete setting of the existing Coq system., L’assistant de preuve Coq permet de s’assurer mécaniquement de la correction de chaque étape de raisonnement dans une preuve. Ce système peut également servir au développement de programmes certifiés. En effet, Coq utilise en interne un langage typé dérivé du λ-calcul, le calcul des constructions inductives (CIC). Ce langage est directement utilisable pour programmer, et un mécanisme — l’extraction — permet de traduire les programmes CIC vers des langages à plus large audience tels qu’OCaml, Haskell ou Scheme.L’extraction n’est pas un simple changement de syntaxe : CIC dispose d’un système de types très riche, mais en contrepartie, des entités purement logiques peuvent apparaître dans les programmes et impacter leurs performances. L’extraction se charge également d’effacer ces parties logiques.Dans cette thèse, nous nous attaquons à la certification de l’extraction elle-même. Nous avons prouvé sa correction dans le cadre d’une formalisation entière de Coq en Coq. Cette formalisation ne correspond pas exactement au CIC implanté dans Coq, mais nous avons tout de même réalisé notre étude avec l’implantation concrète de Coq en tête. Nous proposons également une nouvelle méthode de certification des programmes extraits, dans le cadre concret du système Coq existant.

This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to build a logic from a programming language, both described as pure type systems. This logic provides formulas to express properties of programs and offers a formal framework that allows us to develop a theory of realizability in which realizers of formulas are exactly programs of the starting programming language. In our framework, the standard representation theorems of Gödel's system T and Girard's system F may be seen as two instances of a more general theorem. Then, we explain how the so-called « logical relations » of parametricity theory may be expressed in terms of realizability, which shows that the generated logic provides an adequate framework for developping a general theory of parametricity. Finally, we show how this parametricity theory can be adapted to the underlying type system of the proof assistant Coq and we give an original example of application of parametricity theory to the formalization of mathematics., Cette thèse porte sur l’adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d’un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques.

Pedagogical formal systems have appeared recently for propositional calculus (up to the higher order), and it consists of systematically give examples of introduced notions (hypotheses). Formally, it means that to use a set Delta of formulas as hypotheses, one must first give a substitution sigma such that all the instances of formulas sigma(Delta) can be proved. This neccesity of giving examples has been pointed out by Poincaré (1913) as a common-sense practice: a definition of an object by means of assumptions has interest only if such an object can be constructed. This restriction applied to intuitionistic formal systems is consistent with the idea of negationless mathematics advocated by Griss (1946) in the middle of the past century, and shown as a more deep view of intuitionism. Through the Curry-Howard isomorphism (1980), the computational counterpart is the utility of programs defined in the associated functional systems: every function can be applied to a closed value. First results concerning propositional calculi up to the second-order has recently been published by Colson and Michel (2007, 2008, 2009). In this thesis we present an attempt to standardize and to extend to the Calculus of Constructions (CC) those previous results. First a formal and precise definition of pedagogical sub-systems of the Calculus of Constructions is introduced, and different such sub-systems are exhibited as examples., Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version approfondie de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondants: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans cette thèse une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple.

This thesis presents advances in the use of Canonical Structures, a programming language construct of the Coq proof assistant equivalent to the notion of type classes. It provides a new model for developping hierarchies of mathematical structures using dependent records, and, as an illustration, reformulates the common formal proof of the correctness of the RSA cryptosystem, providing facilities for algebraic reasoning along with a formalization in type theory of the necessary mathematical notions (including cyclic groups, automorphism groups, group isomorphisms). We provide an extension of the Canonical Structure inference mechanism using phantom types, and apply it to treating the notion of partial functions. Next, we consider a generic treatment of several forms of subgroup definitions occurring in the formalization of the Feit-Thompson theorem, a large library of fomalized algebra developed in the Mathematical Components team at the MSR-INRIA joint laboratory. We show that a unified treatment of those 16 subgroups allows us to shorten menial proofs and obtain more composable definitions. We formalize a correspondence between the study of those group functorials, and some common and useful group-theoretic properties represented as the class of groups verifying them. We conclude in exploring the possibilities for analyzing the functoriality of those definitions by inspecting their type, and suggest a path towards obtaining instances of a parametricity result in Coq.; Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.

This thesis presents advances in the use of Canonical Structures, a programming language construct of the Coq proof assistant equivalent to the notion of type classes. It provides a new model for developping hierarchies of mathematical structures using dependent records, and, as an illustration, reformulates the common formal proof of the correctness of the RSA cryptosystem, providing facilities for algebraic reasoning along with a formalization in type theory of the necessary mathematical notions (including cyclic groups, automorphism groups, group isomorphisms). We provide an extension of the Canonical Structure inference mechanism using phantom types, and apply it to treating the notion of partial functions. Next, we consider a generic treatment of several forms of subgroup definitions occurring in the formalization of the Feit-Thompson theorem, a large library of fomalized algebra developed in the Mathematical Components team at the MSR-INRIA joint laboratory. We show that a unified treatment of those 16 subgroups allows us to shorten menial proofs and obtain more composable definitions. We formalize a correspondence between the study of those group functorials, and some common and useful group-theoretic properties represented as the class of groups verifying them. We conclude in exploring the possibilities for analyzing the functoriality of those definitions by inspecting their type, and suggest a path towards obtaining instances of a parametricity result in Coq.; Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.

The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.; L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.

The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.; L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.

In recent years, the emergence of feature rich and mature interactive proof assistants has enabled large formalization efforts of high-profile conjectures and results previously established only by pen and paper. A medley of incompatible and philosophically diverging logics are at the core of all these proof assistants. Cousineau and Dowek (2007) have proposed the λΠ-calculus modulo as a universal target framework for other front-end proof languages and environments. We explain in this thesis how this particularly simple formalism allows for a small, modular and efficient proof checker upon which the consistency of entire systems can be made to rely upon. Proofs increasingly rely on computation both in the large, as exemplified by the proof of the four colour theorem by Gonthier (2007), and in the small following the SSReflect methodoly and supporting tools. Encoding proofs from other systems in the λΠ-calculus modulo bakes yet more computation into the proof terms. We show how to make the proof checking problem manageable by turning entire proof terms into functional programs and compiling them in one go using off-the-shelf compilers for standard programming languages. We use untyped normalization by evaluation (NbE) as an enabling technology and show how to optimize previous instances of it found in the literature. Through a single change to the interpretation of proof terms, we arrive at a representation of proof terms using higher order abstract syntax (HOAS) allowing for a proof checking algorithm devoid of any explicit typing context for all Pure Type Systems (PTS). We observe that this novel algorithm is a generalization to dependent types of a type checking algorithm found in the HOL proof assistants enabling on-the-fly checking of proofs. We thus arrive at a purely functional system with no explicit state, where all proofs are checked by construction. We formally verify in Coq the correspondence of the type system on higher order terms lying behind this algorithm with respect to the standard typing rules for PTS. This line of work can be seen as connecting two historic strands of proof assistants: LCF and its descendents, where proofs of untyped or simply typed formulae are checked by construction, versus Automath and its descendents, where proofs of dependently typed terms are checked a posteriori. The algorithms presented in this thesis are at the core of a new proof checker called Dedukti and in some cases have been transferred to the more mature platform that is Coq. In joint work with Denes, we show how to extend the untyped NbE algorithm to the syntax and reduction rules of the Calculus of Inductive Constructions (CIC). In joint work with Burel, we generalize previous work by Cousineau and Dowek (2007) on the embedding into the λΠ-calculus modulo of a large class of PTS to inductive types, pattern matching and fixpoint operators.; Ces dernières années ont vu l'émergence d'assistants interactifs de preuves riches en fonctionnalités et d'une grande maturité d'implémentation, ce qui a permis l'essor des grosses formalisations de résultats papier et la résolution de conjectures célèbres. Mais autant d'assistants de preuves reposent sur presque autant de logiques comme fondements théoriques. Cousineau et Dowek (2007) proposent le λΠ-calcul modulo comme un cadre universel cible pour tous ces environnement de démonstration. Nous montrons dans cette thèse comment ce formalisme particulièrement simple admet une implémentation d'un vérificateur de taille modeste mais pour autant modulaire et efficace, à la correction de laquelle on peut réduire la cohérence de systèmes tout entiers. Un nombre croissant de preuves dépendent de calculs intensifs comme dans la preuve du théorème des quatre couleurs de Gonthier (2007). Les méthodologies telles que SSReflect et les outils attenants privilégient les preuves contenant de nombreux petits calculs plutôt que les preuves purement déductives. L'encodage de preuves provenant d'autres systèmes dans le λΠ-calcul modulo introduit d'autres calculs encore. Nous montrons comment gérer la taille de ces calculs en interprétant les preuves tout entières comme des programmes fonctionnels, que l'on peut compiler vers du code machine à l'aide de compilateurs standards et clé-en-main. Nous employons pour cela une variante non typée de la normalisation par évaluation (NbE), et montrons comment optimiser de précédentes formulation de celle-ci. Au travers d'une seule petite modification à l'interprétation des termes de preuves, nous arrivons aussi à une représentation des preuves en syntaxe abstraite d'ordre supérieur (HOAS), qui admet naturellement un algorithme de typage sans aucun contexte de typage explicite. Nous généralisons cet algorithme à tous les systèmes de types purs (PTS). Nous observons que cet algorithme est une extension à un cadre avec types dépendants de l'algorithme de typage des assistants de preuves de la famille HOL. Cette observation nous amène à développer une architecture à la LCF pour une large classe de PTS, c'est à dire une architecture où tous les termes de preuves sont corrects par construction, a priori donc, et n'ont ainsi pas besoin d'être vérifié a posteriori. Nous prouvons formellement en Coq un théorème de correspondance entre les système de types sans contexte et leur pendant standard avec contexte explicite. Ces travaux jettent un pont entre deux lignées historiques d'assistants de preuves : la lignée issue de LCF à qui nous empruntons l'architecture du noyau, et celle issue de Automath, dont nous héritons la notion de types dépendants. Les algorithmes présentés dans cette thèse sont au coeur d'un nouveau vérificateur de preuves appelé Dedukti et ont aussi été transférés vers un système plus mature : Coq. En collaboration avec Dénès, nous montrons comment étendre la NbE non typée pour gérer la syntaxe et les règles de réduction du calcul des constructions inductives (CIC). En collaboration avec Burel, nous généralisons des travaux précédents de Cousineau et Dowek (2007) sur l'encodage dans le λΠ-calcul modulo d'une large classe de PTS à des PTS avec types inductifs, motifs de filtrage et opérateurs de point fixe.

In recent years, the emergence of feature rich and mature interactive proof assistants has enabled large formalization efforts of high-profile conjectures and results previously established only by pen and paper. A medley of incompatible and philosophically diverging logics are at the core of all these proof assistants. Cousineau and Dowek (2007) have proposed the λΠ-calculus modulo as a universal target framework for other front-end proof languages and environments. We explain in this thesis how this particularly simple formalism allows for a small, modular and efficient proof checker upon which the consistency of entire systems can be made to rely upon. Proofs increasingly rely on computation both in the large, as exemplified by the proof of the four colour theorem by Gonthier (2007), and in the small following the SSReflect methodoly and supporting tools. Encoding proofs from other systems in the λΠ-calculus modulo bakes yet more computation into the proof terms. We show how to make the proof checking problem manageable by turning entire proof terms into functional programs and compiling them in one go using off-the-shelf compilers for standard programming languages. We use untyped normalization by evaluation (NbE) as an enabling technology and show how to optimize previous instances of it found in the literature. Through a single change to the interpretation of proof terms, we arrive at a representation of proof terms using higher order abstract syntax (HOAS) allowing for a proof checking algorithm devoid of any explicit typing context for all Pure Type Systems (PTS). We observe that this novel algorithm is a generalization to dependent types of a type checking algorithm found in the HOL proof assistants enabling on-the-fly checking of proofs. We thus arrive at a purely functional system with no explicit state, where all proofs are checked by construction. We formally verify in Coq the correspondence of the type system on higher order terms lying behind this algorithm with respect to the standard typing rules for PTS. This line of work can be seen as connecting two historic strands of proof assistants: LCF and its descendents, where proofs of untyped or simply typed formulae are checked by construction, versus Automath and its descendents, where proofs of dependently typed terms are checked a posteriori. The algorithms presented in this thesis are at the core of a new proof checker called Dedukti and in some cases have been transferred to the more mature platform that is Coq. In joint work with Denes, we show how to extend the untyped NbE algorithm to the syntax and reduction rules of the Calculus of Inductive Constructions (CIC). In joint work with Burel, we generalize previous work by Cousineau and Dowek (2007) on the embedding into the λΠ-calculus modulo of a large class of PTS to inductive types, pattern matching and fixpoint operators.; Ces dernières années ont vu l'émergence d'assistants interactifs de preuves riches en fonctionnalités et d'une grande maturité d'implémentation, ce qui a permis l'essor des grosses formalisations de résultats papier et la résolution de conjectures célèbres. Mais autant d'assistants de preuves reposent sur presque autant de logiques comme fondements théoriques. Cousineau et Dowek (2007) proposent le λΠ-calcul modulo comme un cadre universel cible pour tous ces environnement de démonstration. Nous montrons dans cette thèse comment ce formalisme particulièrement simple admet une implémentation d'un vérificateur de taille modeste mais pour autant modulaire et efficace, à la correction de laquelle on peut réduire la cohérence de systèmes tout entiers. Un nombre croissant de preuves dépendent de calculs intensifs comme dans la preuve du théorème des quatre couleurs de Gonthier (2007). Les méthodologies telles que SSReflect et les outils attenants privilégient les preuves contenant de nombreux petits calculs plutôt que les preuves purement déductives. L'encodage de preuves provenant d'autres systèmes dans le λΠ-calcul modulo introduit d'autres calculs encore. Nous montrons comment gérer la taille de ces calculs en interprétant les preuves tout entières comme des programmes fonctionnels, que l'on peut compiler vers du code machine à l'aide de compilateurs standards et clé-en-main. Nous employons pour cela une variante non typée de la normalisation par évaluation (NbE), et montrons comment optimiser de précédentes formulation de celle-ci. Au travers d'une seule petite modification à l'interprétation des termes de preuves, nous arrivons aussi à une représentation des preuves en syntaxe abstraite d'ordre supérieur (HOAS), qui admet naturellement un algorithme de typage sans aucun contexte de typage explicite. Nous généralisons cet algorithme à tous les systèmes de types purs (PTS). Nous observons que cet algorithme est une extension à un cadre avec types dépendants de l'algorithme de typage des assistants de preuves de la famille HOL. Cette observation nous amène à développer une architecture à la LCF pour une large classe de PTS, c'est à dire une architecture où tous les termes de preuves sont corrects par construction, a priori donc, et n'ont ainsi pas besoin d'être vérifié a posteriori. Nous prouvons formellement en Coq un théorème de correspondance entre les système de types sans contexte et leur pendant standard avec contexte explicite. Ces travaux jettent un pont entre deux lignées historiques d'assistants de preuves : la lignée issue de LCF à qui nous empruntons l'architecture du noyau, et celle issue de Automath, dont nous héritons la notion de types dépendants. Les algorithmes présentés dans cette thèse sont au coeur d'un nouveau vérificateur de preuves appelé Dedukti et ont aussi été transférés vers un système plus mature : Coq. En collaboration avec Dénès, nous montrons comment étendre la NbE non typée pour gérer la syntaxe et les règles de réduction du calcul des constructions inductives (CIC). En collaboration avec Burel, nous généralisons des travaux précédents de Cousineau et Dowek (2007) sur l'encodage dans le λΠ-calcul modulo d'une large classe de PTS à des PTS avec types inductifs, motifs de filtrage et opérateurs de point fixe.

This dissertation is about the investigation of the concept of conversion that lies within any kind of dependently typed systems. Several presentations of those systems have been studied for various purposes: typing, proof search, logical coherence... Each presentation embeds its own notion of equality, tuned for its own goal. However, the question to know whereas all those representations in fact reflecting the same theory is not yet proved. We will focus here on a quite large family of systems called Pure Type Systems, and we will prove that all of their usual presentations are equivalent, by exhibiting a constructive translation from a representation to the other. All of those translations are based on the behaviour of the equality and the ways to translate them. Therefore, this work will focus on the properties of the equality, and we will prove that it is possible to type any syntactic equality into a semantic one, which is enough to translate any system into another one. Moreover, all of this thesis has been verified and proved correct with the Coq proof assistant, which has also been used during the development of the proofs.; 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. ~

This dissertation is about the investigation of the concept of conversion that lies within any kind of dependently typed systems. Several presentations of those systems have been studied for various purposes: typing, proof search, logical coherence... Each presentation embeds its own notion of equality, tuned for its own goal. However, the question to know whereas all those representations in fact reflecting the same theory is not yet proved. We will focus here on a quite large family of systems called Pure Type Systems, and we will prove that all of their usual presentations are equivalent, by exhibiting a constructive translation from a representation to the other. All of those translations are based on the behaviour of the equality and the ways to translate them. Therefore, this work will focus on the properties of the equality, and we will prove that it is possible to type any syntactic equality into a semantic one, which is enough to translate any system into another one. Moreover, all of this thesis has been verified and proved correct with the Coq proof assistant, which has also been used during the development of the proofs.; 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. ~

In order to specify the behavior of programming languages, to investigate their properties and to allow certification of their implementations, one studies formal models of existing programming languages. This study splits into the study of syntax and semantics, where the latter is based on appropriate formal models for the syntax. This PhD thesis is located in the syntactic part and is mainly concerned with two approaches to abstract syntax with variable binding. Both make use of the language of category theory. The first one is in the spirit of the category theoretic approach to algebraic theories. The second one is based on the notion of monads and introduces modules on monads instead of working with functors and their algebras. Furthermore the latter approach is adapted to a larger class of typed syntax with types depending on terms.; Afin de spécifier le comportement des langages de programmation, de préciser leurs propriétés et de certifier leurs implémentations, on étudie des modèles formels des langages de programmation. L'étude se divise en l'étude de la syntaxe et en celle de la sémantique. La deuxième est basée sur des modèles formels de la syntaxe. Cette thèse de doctorat se situe dans l'étude de la syntaxe et est consacrée principalement à deux approches à la syntaxe abstraite typée avec liaison de variables. Ces deux approches utilisent le langage de la théorie des catégories. La premièere approche est dans l'esprit de l'approche catégorique aux théories alébriques. La deuxième est basée sur la notion de monade et introduit la notion d'un module sur une monade qui remplacent les foncteurs et leurs algèbres. En outre la deuxième approche est adaptée pour une classe plus large de syntaxes typées où les types dépendent des termes.

In order to specify the behavior of programming languages, to investigate their properties and to allow certification of their implementations, one studies formal models of existing programming languages. This study splits into the study of syntax and semantics, where the latter is based on appropriate formal models for the syntax. This PhD thesis is located in the syntactic part and is mainly concerned with two approaches to abstract syntax with variable binding. Both make use of the language of category theory. The first one is in the spirit of the category theoretic approach to algebraic theories. The second one is based on the notion of monads and introduces modules on monads instead of working with functors and their algebras. Furthermore the latter approach is adapted to a larger class of typed syntax with types depending on terms.; Afin de spécifier le comportement des langages de programmation, de préciser leurs propriétés et de certifier leurs implémentations, on étudie des modèles formels des langages de programmation. L'étude se divise en l'étude de la syntaxe et en celle de la sémantique. La deuxième est basée sur des modèles formels de la syntaxe. Cette thèse de doctorat se situe dans l'étude de la syntaxe et est consacrée principalement à deux approches à la syntaxe abstraite typée avec liaison de variables. Ces deux approches utilisent le langage de la théorie des catégories. La premièere approche est dans l'esprit de l'approche catégorique aux théories alébriques. La deuxième est basée sur la notion de monade et introduit la notion d'un module sur une monade qui remplacent les foncteurs et leurs algèbres. En outre la deuxième approche est adaptée pour une classe plus large de syntaxes typées où les types dépendent des termes.

In this thesis we propose and study several deduction systems that mix deduction and computation. Deduction modulo proposes to translate a computational power through a rewriting system. We present the dual concept called superdeduction. It translates a deductive power into custom inference rules that enrich the deduction system. These computational and deductive powers modify the representation of proofs as well as their interaction through cut-elimination processes. Strong normalisation or cut-admissibility may be lost and therefore appear as intrinsic properties of theories represented as rewriting systems. We prove that certain criteria imply these properties by defining a proof-term language for superdeduction and by studying the permutability of inferences in classical sequent calculus. Our attention is focused on classical sequent calculi and on the representation of proofs in such systems. Other related paradigms are considered, namely proof-nets and focusing. We compare this latter approach with superdeduction. We consequently reforge the superdeduction paradigm on top of a multifocusing system for classical logic. We demonstrate the benefits of this approach by proving the completeness of the obtained deduction systems., Cette thèse propose et étudie de nouveaux systèmes déductifs mêlant calculs et déductions. La déduction modulo est un premier formalisme qui traduit un pouvoir calculatoire grâce à un système de réécriture. Nous présentons un paradigme dual appelé superdéduction qui traduit un pouvoir déductif par de nouvelles inférences. Ces pouvoirs calculatoires et déductifs modifient la représentation des preuves et leur interaction par les processus d'élimination des coupures. La normalisation forte ou l'admissibilité des coupures ne sont plus garanties et apparaissent alors comme des propriétés intrinsèques des théories représentées sous forme de systèmes de réécriture. Nous démontrons que certains critères permeent d'assurer ces propriétés, notamment en définissant un langage de termes de preuve pour la superdéduction et en étudiant la permutabilité des inférences en calcul des séquents classique. Notre attention est focalisée sur les calculs des séquents classiques et la représentation des preuves dans de tels systèmes. D'autres formalismes connexes sont envisagés, notamment les réseaux de preuve et le focusing. Nous comparons cette dernière approe à la superdéduction, ce qui nous amène à proposer une refonte du paradigme de superdéduction basée sur un système de multifocusing pour la logique classique. Nous en montrons les effets bénéfiques en démontrant la complétude des systèmes déductifs obtenus.

Type Theory lies on the crossroad of Logics, Mathematics and Computer Science. It may be used to develop the "zero-error" programs. The aim of this thesis is to study an extension of a system with dependent types called UTT (including inductive types) that is obtained by adding to the rewrite relation of UTT new rewrite rules concerning finite types. We check that Strong Normalization, Church-Rosser property and Subject Reduction are preserved. We consider another extension by Coercive Subtyping that is seen as an abbreviation mechanism and give a conservativity proof for the system enriched by Coercive Subtyping with respect to underlying UTT (with an without new rewrite rules). The interest of such a system is that it will improve the efficiency of proof assistants and provides a general framework for treatment of the problems involving finite types (combinatorics, graphs etc).; La théorie des types est une discipline au croisement de la logique, des mathématiques et de l'informatique. Elle peut servir de support au développement de programme "zéro faute". L'objet de cette thèse est d'étudier l'extension d'un système aux types dépendants UTT (comprenant notamment des types inductifs) par une relation de récriture concernant un fragment du calcul, à savoir les types finis. Nous nous assurons d'abord que les propriétés de normalisation forte, de confluence et de préservation du type sont toujours préservées malgré l'ajout de la réduction. Ensuite nous enrichissons ce système par la notion de sous-typage coercitif vue comme un mécanisme d'abréviation et effectuons la preuve de conservativité pour le système enrichi du sous-typage par rapport au système de base. L'intérêt d'un tel système est qu'il améliora l'efficacité des assistants à la preuve et offrira un bon cadre pour l'étude des problèmes faisant intervenir des ensembles finis (combinatoire, manipulation de graphe etc).

In "The Continuum", Hermann Weyl gives new bases to the notions of set and function. With them, he constructs mathematics close to physics and solves the continuum problem. Those new notions are so unusual with respect to Set Theory that they are often misunderstood. We propose to explain the meaning of Weyl's reform of those notions. We first make a synthesis of his main epistemological thesis, and then propose a comparative approach to stress the distance between the mathematical and logical principles of "The Continuum", those of Set Theory, and those of Russell's ramified theory of types. Our discussion will be centred on the distinction between intension and extension, and on the place that Weyl gives to natural numbers for the foundations of analysis., Dans le Continu, Hermann Weyl donne une nouvelle assise aux notions d'ensemble et de fonction, pour assurer aux mathématiques leur applicabilité à la physique, et résoudre ainsi le problème du continu. Les notions introduites, éloignées de la théorie des ensembles, prêtent à confusion et à multiples interprétations. Nous nous proposons d'éclairer le sens du déplacement que Weyl opère dans ces notions. Nous présentons une synthèse des thèses épistémologiques soutenues dans "Le Continu" et résolvons certains problèmes interprétatifs. Par une approche comparative, nous soulignons l'écart entre les principes logico-mathématiques du "Continu", ceux de la théorie des ensembles, et ceux de la théorie des types ramifiés de B. Russell. Nous nous centrons sur la distinction entre intension et extension, et sur la place attribuée aux entiers naturels pour le fondement des mathématiques.

Due to the new requirements of modern software, researchers in software engineering have created more efficient development methods based on the concept of modeling (for example, the MDA) to control every stage of development. From a theoretical point of view, these methods are based on graphs and graph transformations. The theoretical difficulty lies in adding on these graphs data on which it must be possible to do computations. Our work has focused on developing a mathematical framework to implement these changes. The theories of categories (through the double pushout) and inductive types (very expressive computation functions) allowed us to provide a unified solution to this problem in which a single operation can transform the structure and compute with the attributes. In addition, the usual properties of rewriting systems are checked.; 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.

The goal of this thesis is to develop a logical system in which formal proofs of mathematical statements can be carried out in a way which is close to mathematical practice. Our main contribution is the definition and study of a new calculus, the Calculus of Congruent and Inductive Constructions, an extension of the Calculus of Inductive Constructions (CIC) integrating in its computational part the entailment relation - via decision procedures - of a first order theory over equality. A major technical innovation of this work lies in the computational mechanism: goals are sent to the decision procedure together with a set of user hypotheses available from the current context. Our main results show that this extension of CIC does not compromise its main properties: confluence, strong normalization, consistency and decidability of proof checking are all preserved (as soon as the incorporated theory is itself decidable). As such, our calculus can be seen as a decidable restriction of the Extensional Calculus of Constructions. It can therefore serve as the basis for an extension of the Coq proof assistant.; Le but de cette thèse est l'étude d'un système logique formel dans lequel les preuves formelles de propriétés mathématiques sont menées dans un style plus proches des pratiques des mathématiciens. Notre principal apport est la définition et l'étude du Calcul des Constructions Inductives Congruentes, une extension du Calcul des Constructions Inductives (CIC), intégrant au sein de son mécanisme de calcul des procédures de décisions pour des théories equationnelles au premier ordre. Nous montrons que ce calcul possède toutes les propriétés attendues: confluence, normalisation forte, cohérence logique et décidabilité de la vérification de types sont préservées. En tant que tel, notre calcul peut être vu comme une restriction décidable du Calcul des Constructions Extentionnelles et peut servir comme base pour l'extension de l'assistant à la preuve Coq.

The goal of this thesis is to develop a logical system in which formal proofs of mathematical statements can be carried out in a way which is close to mathematical practice. Our main contribution is the definition and study of a new calculus, the Calculus of Congruent and Inductive Constructions, an extension of the Calculus of Inductive Constructions (CIC) integrating in its computational part the entailment relation - via decision procedures - of a first order theory over equality. A major technical innovation of this work lies in the computational mechanism: goals are sent to the decision procedure together with a set of user hypotheses available from the current context. Our main results show that this extension of CIC does not compromise its main properties: confluence, strong normalization, consistency and decidability of proof checking are all preserved (as soon as the incorporated theory is itself decidable). As such, our calculus can be seen as a decidable restriction of the Extensional Calculus of Constructions. It can therefore serve as the basis for an extension of the Coq proof assistant.; Le but de cette thèse est l'étude d'un système logique formel dans lequel les preuves formelles de propriétés mathématiques sont menées dans un style plus proches des pratiques des mathématiciens. Notre principal apport est la définition et l'étude du Calcul des Constructions Inductives Congruentes, une extension du Calcul des Constructions Inductives (CIC), intégrant au sein de son mécanisme de calcul des procédures de décisions pour des théories equationnelles au premier ordre. Nous montrons que ce calcul possède toutes les propriétés attendues: confluence, normalisation forte, cohérence logique et décidabilité de la vérification de types sont préservées. En tant que tel, notre calcul peut être vu comme une restriction décidable du Calcul des Constructions Extentionnelles et peut servir comme base pour l'extension de l'assistant à la preuve Coq.