Le but principal de cette thèse est de définir une extension de la traduction de double-négation de Gödel à tous les types tronqués, dans le contexte de la théorie des types homotopique. Ce but utilisera des théories déjà existantes, comme la théorie des faisceaux de Lawvere-Tierney, quenous adapterons à la théorie des types homotopiques. En particulier, on définira le fonction de faisceautisation de Lawvere-Tierney, qui est le principal théorème présenté dans cette thèse.Pour le définir, nous aurons besoin de concepts soit déjà définis en théorie des types, soit non existants pour l’instant. En particulier, on définira une théorie des colimits sur des graphes, ainsi que leur version tronquée, et une notion de modalités tronquées basée sur la définition existante de modalité.Presque tous les résultats présentés dans cette thèse sont formalisée avec l’assistant de preuve Coq, muni de la librairie [HoTT/Coq] / The main goal of this thesis is to define an extension of Gödel not-not translation to all truncated types, in the setting of homotopy type theory. This goal will use some existing theories, like Lawvere-Tierney sheaves theory in toposes, we will adapt in the setting of homotopy type theory. In particular, we will define a Lawvere-Tierney sheafification functor, which is the main theorem presented in this thesis.To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities.Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq]

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.

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 / 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

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 permettent 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 approche à 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. / 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 une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité modifiée est introduite et étudiée. Un codage imprédicatif d'une large classe de définitions inductives est proposé.

Cette thèse porte sur la construction d'un environnement pour développer des librairies de calcul formel certifié. Nous présentons d'abord les espèces, structures servant à décrire des spécifications par héritage multiple, raffinement et paramétrisation. Les collections, construites par encapsulation d'espèces constituent la librairie utilisateur. Nous définissons également les analyses statiques garantissant la correction d'une définition d'espèce. Ensuite, nous étudions la compilation des espèces et collections vers le langage d'exécution OCAML, en utilisant les objets et modules OCAML. Puis nous détaillons la traduction dans le langage de preuves COQ, la liaison retardée étant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les exécutables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme à la formalisation des espèces faites auparavant en COQ.

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.

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.

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

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.<br /><br /> 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.<br /><br /> 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.