Les systèmes basés sur la Théorie des Types prennent une importance considérable tant pour la vérification de programmes qu'en tant qu'outils permettant la preuve formelle de théorèmes mettant en jeu des calculs complexes. Ces systèmes nécessitent aujourd'hui une grande expertise pour être utilisés efficacement. Nous développons des constructions de haut niveau permettant d'utiliser les langages basés sur les théories des types dépendants aussi simplement que les langages de programmation fonctionnels usuels, sans sacrifier pour autant la richesse des constructions disponibles dans les premiers. Nous étudions un nouveau langage permettant l'écriture de programmes certifiés en ne donnant que leur squelette algorithmique et leur spécification. Le typage dans ce système donne lieu à la génération automatique d'obligations de preuve pouvant être résolues a posteriori. Nous démontrons les propriétés métathéoriques essentielles du système, dont les preuves sont partiellement mécanisées, et détaillons son implémentation dans l'assistant de preuve Coq. D'autre part, nous décrivons l'intégration et l'extension d'un système de "Type Classes" venu d'Haskell à Coq via une simple interprétation des constructions liées aux classes dans la théorie des types sous-jacente. Nous démontrons l'utilité des classes de types dépendantes pour la spécification et la preuve et présentons une implémentation économique et puissante d'une tactique de réécriture généralisée basée sur les classes. Nous concluons par la mise en œuvre de l'ensemble de ces contributions lors du développement d'une bibliothèque certifiée de manipulation d'une structure de données complexe, les "Finger Trees".

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

Les assistants de preuve basés sur des théories des types dépendants sont de plus en plus utilisé comme un outil pour développer programmes certifiés. Un exemple réussi est l'assistant de preuves Coq, fondé sur le Calcul des Constructions Inductives (CCI). Coq est un langage de programmation fonctionnel dont un expressif système de type qui permet de préciser et de démontrer des propriétés des programmes dans une logique d'ordre supérieur. Motivé par le succès de Coq et le désir d'améliorer sa facilité d'utilisation, dans cette thèse nous étudions certaines limitations des implémentations actuelles de Coq et sa théorie sous-jacente, CCI. Nous proposons deux extension de CCI que partiellement resourdre ces limitations et que on peut utiliser pour des futures implémentations de Coq. Nous étudions le problème de la terminaison des fonctions récursives. En Coq, la terminaison des fonctions récursives assure la cohérence de la logique sous-jacente. Les techniques actuelles assurant la terminaison de fonctions récursives sont fondées sur des critères syntaxiques et leurs limitations apparaissent souvent dans la pratique. Nous proposons une extension de CCI en utilisant un mécanisme basé sur les type pour assurer la terminaison des fonctions récursives. Notre principale contribution est une preuve de la normalisation forte et la cohérence logique de cette extension. Nous étudions les définitions par filtrage dans le CCI. Avec des types dépendants, il est possible d'écrire des définitions par filtrage plus précises, par rapport à des langages de programmation fonctionnels Haskell et ML. Basé sur le succès des langages de programmation avec types dépendants, comme Epigram et Agda, nous développons une extension du CCI avec des fonctions similaires.

Dans ce mémoire, je présente une technique pour combiner du code de bas niveau à un langage purement fonctionnel avec types dépendants. Par code de bas niveau, je veux dire n’importe quel programme écrit dans un langage qui permet le contrôle direct des ressources de la machine. En particulier, ce texte s’intéresse à la gestion de la mémoire. Plus concrètement, un programmeur C contrôle l’endroit et le moment où un bloc de mémoire est alloué, ainsi que la façon dont l’objet est initialisé. Par exemple, on peut allouer de l’espace sur la pile pour immédiatement l’initialiser avec un memcpy. Alternativement, on peut allouer un bloc sur le tas et l’initialiser champ par champ plus tard. Pour certaines applications où la mémoire est limitée ou la performance importante, ce choix est important. Un tel niveau de contrôle n’est pas disponible dans les langages de haut niveau, sauf pour quelques exceptions. Les langages fonctionnels comme OCaml ou Haskell découragent ou même interdisent de modifier les champs d’un objet. C’est encore plus vrai pour les langages à types dépendants où la mutation est l’éléphant dans le magasin de porcelaine de la cohérence. C’est un choix de design intentionnel. Un programme pur est plus facile à comprendre et analyser, mais comment séparer l’initialisation de l’allocation quand un objet ne peut pas changer ? Ce mémoire essaie de démontrer que ce n’est pas parce que c’est impossible, mais parce que ces langages ne sont pas habituellement utilisés dans un contexte où c’est nécessaire. Par contre, ce n’est pas facile non plus. Pour garantir la sécurité et la cohérence, il faut modéliser l’état d’un objet partiellement initialisé au niveau des types, ce que la plupart des langages ont de la peine à faire. La combinaison du manque de nécessité et de la lourdeur syntaxique et conceptuelle est la raison pour laquelle cette fonctionnalité est souvent absente. Pour y parvenir, nous prenons un langage à types dépendants, Typer, et nous y ajoutons le nécessaire pour récupérer une partie du contrôle abandonné dans le design original. Nous permettons au programmeur d’allouer des blocs de mémoire et de les initialiser graduellement plus tard, sans compromettre les propriétés de sécurité du programme. Concrètement, nous utilisons les monades, un concept de la théorie des catégories déjà utilisé pour la modélisation d’effets de bord, pour limiter les mutations aux endroits sécuritaires. / In this thesis, I will demonstrate how to combine low-level code with dependent types. By low-level code, I mean any program authored in a language that allows direct control of computer resources. In particular, this text will focus on memory management. Specifically, a C programmer has control over the location and time when a block of memory is allocated, as well as how it is initialized. For instance, it is possible to allocate stack space to immediately initialize it with an invocation of memcpy. Alternatively, one can allocate heap spate and initialize it field by field later. For some applications where memory is constrained or performance is important, this choice can matter. This level of control is not available in high-level languages, barring a few exceptions. Functional languages such as OCaml or Haskell discourage or simply forbid the mutation of objects. This is especially the case in dependently typed languages where mutation is the bull in the china shop of consistency. This is a deliberate choice as a pure program is easier to understand and reason about. However, having allocation and initialization done in two distinct steps seems impossible in this situation. This thesis shows that this is not impossible, it is simply done this way because these kinds of languages are seldom used in a context where such control is necessary. This does not mean though that adding this feature is easy. If we are to guarantee both safety and consistency, we need to keep track of the initialization state at the type level. Most languages struggle to do this. Language designers simply forgo this feature because it is not useful to them in addition to being difficult to use. To achieve it, we start with a dependently typed language, Typer, and add back the mechanisms necessary to recover the control relinquished in the original design. We let the programmer allocate blocks of memory to initialize later, without compromising the safety properties of the program. Specifically, we use monads, a concept from category theory, a know technique to model side effects, to limit mutation to situations where it is safe.

Ce travail décrit l’ajout des types quotients dans Typer, un langage avec des types dépendants. Les types quotients permettent aux programmeurs de construire de nouveaux types à base des types existants en redéfinissant la notion d’égalité du type de départ. Typiquement, cela repose sur des relations d’équivalence définies sur le type de base. Les termes qui sont équivalents selon la relation sont donc vus comme égaux dans le type quotient résultant. Par exemple, les nombres rationnels peuvent être définis comme le quotient des paires d’entiers par une relation d’équivalence basée sur le produit en croix. Pour accueillir l’ajout des types quotients dans Typer, on a redéfini et amélioré l’égalité intégré de Typer en s’inspirant de la théorie des types cubique qui a introduit le type d’intervalle et aussi les assistants de preuve qui l’implémentent. De ce fait, la nouvelle égalité de Typer est basé sur les fonctions qui ont comme argument notre nouvelle primitive d’intervalle. Une telle égalité est plus puissante et expressive, elle se prête bien à la construction des preuves liées aux types quotients. Dans ce travail, on s’intéresse également au côté pratique de l’utilisation des types quotients dans un langage tel que Typer, à la fois en termes d’efficacité d’exécution et de facilité d’utilisation pour les développeurs. Les types quotients ne sont pas offerts dans la plupart des langages avec des types dépendants principalement parce que leur utilisation nous entraîne à des obligations de preuves pénibles. Pour faciliter l’utilisation des types quotients, on a fourni une bibliothèque qui simplifie la manipulation des types quotients. On a profité de cette nouvelle addition au langage pour introduire de nouvelles primitives, telle que les nombres rationnels, la troncation propositionnelle, etc. Finalement, ce travail étudie également le développement des preuves en Typer. À notre connaissance, ceci est la première tentative d’écrire une quantité importante de preuves en Typer puisque le langage se veut un langage de programmation à usage général. On décrit notre expérience et les défis auxquels on a dû faire face en cours de route. En outre, on a introduit de nouvelles primitives pour faciliter le développement de preuves en Typer. / This work describes the introduction of quotient types to Typer, a dependently-typed programming language. Quotient types allow programmers to construct new types based on existing types by redefining the notion of equality of the base type. This is typically based on equivalence relations defined on the base type. Terms that are equivalent according to the relation are thus treated as equal in the resulting quotient type. For instance, rational numbers may be defined as the quotient of pairs of integers under an equivalence relation based on cross-multiplication. To better accommodate the introduction of quotient types to Typer, we revamped the built-in equality type by drawing inspiration from cubical type theory that features the interval type and proof assistants that implement it. As such, Typer’s new equality type is based on functions that have our new interval primitive as an argument. Such an equality type is more powerful and expressive, it notably lends itself well to the writing of proofs related to quotient types. In this work, we also investigate the practicality of the usage of quotient types in a language such as Typer, both in terms of run-time efficiency and developer-friendliness. Quotient types do not exist in most modern dependently typed languages, principally because their usage entails burdensome proof obligations. To facilitate the usage of quotient types, we provide a library that helps simplify the manipulation of quotient types. We also leverage this new addition to the language to introduce new built-in types, such as rational numbers, propositional truncation, etc. Finally, this work also explores the development of proofs in Typer, to our knowledge this is the first attempt to write a substantial amount of proofs using the language since the language is primarily intended to be a general-purpose programming language. We describe our experience and the challenges faced in the process. Additionally, we introduce several constructs to streamline proof development in Typer.

Cette thèse, s'intéresse aux systèmes d'interaction, une notion visant à modéliser les interactions entre un système informatique et son environnement.<br /><br />La première partie développe, dans le cadre de la théorie des types de Martin-Löf, la théorie de base des systèmes d'interaction et des constructions inductives et co-inductives qu'ils permettent. On trouve dans cette partie une étude des liens entre systèmes d'interaction et topologies formelles et une formulation (en terme de systèmes d'interaction) d'un théorème de complétude vis-à-vis d'une sémantique topologique des théories géométriques (linéaires).<br /><br />Dans cette étude, la notion complètement standard de simulation, joue un rôle fondamental car elle permet de définir la notion de morphisme entre systèmes d'interaction. Ceci permet d'établir une équivalence entre la catégorie ainsi définie et une autre catégorie, beaucoup plus simple à décrire, celle des transformateurs de prédicats.<br /><br />En traduisant dans ce nouveau vocabulaire les constructions précédentes, on observe que les transformateurs de prédicats forment un nouveau modèle de la logique linéaire, qui est décrit puis étendu au second ordre.<br /><br />Enfin, les propriétés particulières des systèmes d'interaction / transformateurs de prédicats sont mises à profit pour donner une interprétation du lambda-calcul différentiel. Cela suppose d'introduire du non déterminisme, ce que les systèmes d'interaction et les transformateurs de prédicats permettent de faire.

Cette thèse, s'intéresse aux systèmes d'interaction, une notion visant à modéliser les interactions entre un système informatique et son environnement.<br /><br />La première partie développe, dans le cadre de la théorie des types de Martin-Löf, la théorie de base des systèmes d'interaction et des constructions inductives et co-inductives qu'ils permettent. On trouve dans cette partie une étude des liens entre systèmes d'interaction et topologies formelles et une formulation (en terme de systèmes d'interaction) d'un théorème de complétude vis-à-vis d'une sémantique topologique des théories géométriques (linéaires).<br /><br />Dans cette étude, la notion complètement standard de simulation, joue un rôle fondamental car elle permet de définir la notion de morphisme entre systèmes d'interaction. Ceci permet d'établir une équivalence entre la catégorie ainsi définie et une autre catégorie, beaucoup plus simple à décrire, celle des transformateurs de prédicats.<br /><br />En traduisant dans ce nouveau vocabulaire les constructions précédentes, on observe que les transformateurs de prédicats forment un nouveau modèle de la logique linéaire, qui est décrit puis étendu au second ordre.<br /><br />Enfin, les propriétés particulières des systèmes d'interaction / transformateurs de prédicats sont mises à profit pour donner une interprétation du lambda-calcul différentiel. Cela suppose d'introduire du non déterminisme, ce que les systèmes d'interaction et les transformateurs de prédicats permettent de faire.

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.

La modularité est un enjeu important en programmation, surtout quand on l’enrichit avec des preuves, comme dans les langages avec des types dépendants. Typer est un tel langage, et afin d’augmenter sa modularité et de lui ajouter un moyen de faire la surcharge d’opérateurs, on s’inspire d’Agda et Coq et on l’étend avec les arguments instances, qui généralisent les classes de types de Haskell. Un aspect qui distingue notre conception est que comme Typer généralise les définitions, la généralisation des contraintes de classe est grandement facilitée. Pour pouvoir faire les preuves de lois de classes, on doit également ajouter l’élimination dépendante des types inductifs au langage, dont certains aspects sont en retour facilités par les arguments instances. Sur la base de ces deux fonctionnalités, on offre également une solution au problème de la cécité booléenne, tel que décrit par Harper. / Modularity is an important concern for software development, especially when the latter is enriched with proofs in a language with dependent types. Typer is such a language, and in order to increase its modularity, and also provide a way to overload operators, we take inspiration from Agda and Coq and extend it with instance arguments, a generalization of Haskell’s type classes. An aspect that sets our design apart is that since Typer generalizes definitions, it greatly simplifies the generalization of class constraints. In order to allow writing proofs for class laws, we must also implement the dependent elimination of inductive types. In return, instance arguments facilitate some details of dependent elimination. Using both features, we suggest a solution to the problem of Boolean Blindness.

Cette thèse s'intéresse au contenu calculatoire des preuves classiques, et plus spécifiquement aux preuves avec effets de bord et à la réalisabilité classique de Krivine. Le manuscrit est divisé en trois parties, dont la première consiste en une introduction étendue des concepts utilisés par la suite. La seconde partie porte sur l’interprétation calculatoire de l’axiome du choix dépendant en logique classique. Ce travail s'inscrit dans la continuité du système dPAω d'Hugo Herbelin, qui permet d’adapter la preuve constructive de l’axiome du choix en théorie des types de Martin-Löf pour en faire une preuve constructive de l’axiome du choix dépendant dans un cadre compatible avec la logique classique. L'objectif principal de cette partie est de démontrer la propriété de normalisation pour dPAω, sur laquelle repose la cohérence du système. La difficulté d'une telle preuve est liée à la présence simultanée de types dépendants (pour la partie constructive du choix), d'opérateurs de contrôle (pour la logique classique), d'objets co-inductifs (pour "encoder" les fonctions de type N → A par des streams (a₀,a₁,...)) et d'évaluation paresseuse avec partage (pour ces objets co-inductifs). Ces difficultés sont étudiées séparément dans un premier temps. En particulier, on montre la normalisation du call-by-need classique (présenté comme une extension du λµµ̃-calcul avec des environnements partagé), en utilisant notamment des techniques de réalisabilité à la Krivine. On développe ensuite un calcul des séquents classique avec types dépendants, définie comme une adaptation du λµµ̃-calcul, dont la correction est prouvée à l'aide d'une traduction CPS tenant compte des dépendances. Enfin, une variante en calcul des séquents du système dPAω est introduite, combinant les deux points précédents, dont la normalisation est finalement prouvée à l'aide de techniques de réalisabilité. La dernière partie, d'avantage orientée vers la sémantique, porte sur l’étude de la dualité entre l’appel par nom (call-by-name) et l’appel par valeur (call-by-value) dans un cadre purement algébrique inspiré par les travaux autour de la réalisabilité classique (et notamment les algèbres de réalisabilité de Krivine). Ce travail se base sur une notion d'algèbres implicatives développée par Alexandre Miquel, une structure algébrique très simple généralisant à la fois les algèbres de Boole complètes et les algèbres de réalisabilité de Krivine, de manière à exprimer dans un même cadre la théorie du forcing (au sens de Cohen) et la théorie de la réalisabilité classique (au sens de Krivine). Le principal défaut de cette structure est qu’elle est très orientée vers le λ-calcul, et ne permet d’interpréter fidèlement que les langages en appel par nom. Pour remédier à cette situation, on introduit deux variantes des algèbres implicatives les algèbres disjonctives, centrées sur le “par” de la logique linéaire (mais dans un cadre non linéaire) et naturellement adaptées aux langages en appel par nom, et les algèbres conjonctives, centrées sur le “tenseur” de la logique linéaire et adaptées aux langages en appel par valeur. On prouve en particulier que les algèbres disjonctives ne sont que des cas particuliers d'algèbres implicatives et que l'on peut obtenir une algèbre conjonctive à partir d'une algèbre disjonctive (par renversement de l’ordre sous-jacent). De plus, on montre comment interpréter dans ces cadres les fragments du système L de Guillaume Munch-Maccagnoni en appel par valeur (dans les algèbres conjonctives) et en appel par nom (dans les algèbres disjonctives). / This thesis focuses on the computational content of classical proofs, and specifically on proofs with side-effects and Krivine classical realizability. The manuscript is divided in three parts, the first of which consists of a detailed introduction to the concepts used in the sequel.The second part deals with the computational content of the axiom of dependent choice in classical logic. This works is in the continuity of the system dPAω developed Hugo Herbelin. This calculus allows us to adapt the constructive proof of the axiom of choice in Martin-Löf's type theory in order to turn it into a constructive proof of the axiom of dependent choice in a setting compatible with classical logic. The principal goal of this part is to prove the property of normalization for dPAω, on which relies the consistency of the system. Such a proof is hard to obtain, due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of co-inductive objects (in order to "encode" functions of type N → A as streams (a₀,a₁,...)) and of lazy evaluation with sharing (for this co-inductive objects). These difficulties are first studied separately. In particular, we prove the normalization of classical call-by-need (presented as an extension of the λµ̃µ-calculus with shared environments) by means of realizability techniques. Next, we develop a classical sequent calculus with dependent types, defined again as an adaptation of the λµ̃µ-calculus, whose soundness is proved thanks to a CPS translation which takes the dependencies into account. Last, a sequent-calculus variant of dPAω is introduced, combining the two previous systems. Its normalization is finally proved using realizability techniques. The last part, more oriented towards semantics, studies the duality between the call-by-name and the call-by-value evaluation strategies in a purely algebraic setting, inspired from several works around classical realizability (and in particular Krivine realizability algebras). This work relies on the notion of implicative algebras developed by Alexandre Miquel, a very simple algebraic structure generalizing at the same time complete Boolean algebras and Krivine realizability algebras, in such a way that it allows us to express in a same setting the theory of forcing (in the sense of Cohen) and the theory of classical realizability (in the sense of Krivine). The main default of these structures is that they are deeply oriented towards the λ-calculus, and that they only allows to faithfully interpret languages in call-by-name. To remediate the situation, we introduce two variants of implicative algebras: disjunctive algebras, centered on the "par" connective of linear logic (but in a non-linear framework) and naturally adapted to languages in call-by-name; and conjunctives algebras, centered on the "tensor" connective of linear logic and adapted to languages in call-by-value. Amongst other things, we prove that disjunctive algebras are particular cases of implicative algebras and that conjunctive algebras can be obtained from disjunctive algebras (by reversing the underlying order). Moreover, we show how to interpret in these frameworks the fragments of Guillaume Munch-Maccagnoni's system L corresponding to a call-by-value calculus (within conjunctive algebras) and to a call-by-name calculus (within disjunctive algebras).