Les langages de programmation fonctionnels, comme OCaml ou Haskell, reposent sur le lambda calcul en tant que langage noyau. Bien qu'ils aient des stratégies de réduction et des caractéristiques de système de types différentes, leur preuve de correction et de normalisation (en l'absence de réduction) devrait être factorisable. Cette thèse établit une telle factorisation pour des systèmes de types théoriques présentant des types récursifs, du sous-typage, du polymorphisme borné et du polymorphisme contraint. Il est intéressant de remarquer que la correction et la normalisation en réduction forte, implique la correction et la normalisation pour toutes les stratégies usuelles. Notre travail montre qu'une généralisation des coercions actuelles permet de décrire toutes les caractéristiques de systèmes de types citées plus haut de manière effaçable et composable. Nous illustrons ceci en présentant deux systèmes de types concrets : tout d'abord, un système de types explicite avec une forme restreinte d'abstraction sur les coercions pour exprimer le sous-typage et le polymorphisme borné ; puis un système de types implicite sans restriction sur l'abstraction de coercions et qui étend le système explicite avec des types récursifs and du polymorphisme contraint --- mais sans le propriété de préservation du typage. Un résultat annexe est l'adaptation des techniques de step-indexing pour la correction à des calculs en réduction forte.

Cette thèse se place dans le contexte de la vérification déductive des programmes et a pour objectif de formaliser un certain nombre de concepts qui sont mis en œuvre dans l'outil de vérification Why3.L'idée générale est d'explorer des solutions qu'une approche à base de systèmes de types peut apporter à la vérification. Nous commençons par nous intéresser à la notion du code fantôme, une technique implantée dans de nombreux outils de vérification modernes, qui consiste à donner à des éléments de la spécification les apparences d'un code opérationnel. L'utilisation correcte du code fantôme requiert maintes précautions puisqu'il ne doit jamais interférer avec le reste du code. Le premier chapitre est consacré à une formalisation du code fantôme, en illustrant comment un système de types avec effets en permet une utilisation à la fois correcte et expressive. Puis nous nous intéressons à la vérification des programmes manipulant des pointeurs. En présence d'aliasing, c'est-à-dire lorsque plusieurs pointeurs manipulés dans un programme dénotent une même case mémoire, la spécification et la vérification deviennent non triviales. Plutôt que de nous diriger vers des approches existantes qui abordent le problème d'aliasing dans toute sa complexité, mais sortent du cadre de la logique de Hoare, nous présentons un système de types avec effets et régions singletons qui permet d'effectuer un contrôle statique des alias avant même de générer les obligations de preuve. Bien que ce système de types nous limite à des pointeurs dont l'identité peut être connue statiquement, notre observation est qu'il convient à une grande majorité des programmes que l'on souhaite vérifier. Enfin, nous abordons les questions liées à la vérification de programmes conçus de façon modulaire. Concrètement, nous nous intéressons à une situation où il existe une barrière d'abstraction entre le code de l'utilisateur et celui des bibliothèques dont il dépend. Cela signifie que les bibliothèques fournissent à l'utilisateur une énumération de fonctions et de structures de données manipulées, sans révéler les détails de leur implémentation. Le code de l'utilisateur ne peut alors exploiter ces données qu'à travers un ensemble de fonctions fournies. Dans une telle situation, la vérification peut elle-même être modulaire. Du côté de l'utilisateur, la vérification ne doit alors s'appuyer que sur des invariants de type et des contrats de fonctions exposés par les bibliothèques. Du côté de ces dernières, la vérification doit garantir que la représentation concrète raffine correctement les entités exposées, c'est-à-dire en préservant les invariants de types et les contrats de fonctions. Dans le troisième chapitre nous explorons comment un système de types permettant le contrôle statique des alias peut être adapté à la vérification modulaire et le raffinement des structures de données. / This thesis is conducted in the framework of deductive software verification.is aims to formalize some concepts that are implemented in the verification tool Why3. The main idea is to explore solutions that a type system based approach can bring to deductive verification. First, we focus our attention on the notion of ghost code, a technique that is used in most of modern verification tools and which consists in giving to some parts of specification the appearance of operational code. Using ghost code correctly requires various precautions since the ghost code must never interfere with the operational code. The first chapter presents a type system with effects illustrating how ghost code can be used in a way which is both correct and expressive. The second chapter addresses some questions related to verification of programs with pointers in the presence of aliasing, i.e. when several pointers handled by a program denote a same memory cell. Rather than moving towards to approaches that address the problem in all its complexity to the costs of abandoning the framework of Hoare logic, we present a type system with effects and singleton regions which resolves a liasing issues by performing a static control of aliases even before the proof obligations are generated. Although our system is limited to pointers whose identity must be known statically, we observe that it fits for most of the code we want to verify. Finally, we focus our attention on a situation where there exists an abstraction barrier between the user's code and the one of the libraries which it depends on. That means that libraries provide the user a set of functions and of data structures, without revealing details of their implementation. When programs are developed in a such modular way, verification must be modular it self. It means that the verification of user's code must take into account only function contracts supplied by libraries while the verification of libraries must ensure that their implementations refine correctly the exposed entities. The third chapter extends the system presented in the previous chapter with these concepts of modularity and data refinement.

La Programmation Orientée Langage est un paradigme de programmation qui tente, par la technique de méta-programmation, de changer les habitudes des développeurs de systèmes informatiques en leur permettant de "travailler en termes de concepts et notions du problème à résoudre, au lieu d'être toujours obligés de traduire leurs idées aux notions qu'un langage généraliste est capable de comprendre" (Ward et Sergey). Le développement de logiciels passe de ce fait par la conception de langages dédiés : on définit un ou plusieurs langages qui capturent les caractéristiques du domaine étudié, puis on écrit les applications visées en utilisant ces langages. Dans cette thèse, nous proposons une démarche méthodologique de développement logiciel reposant sur ce concept. Il s'agit de conduire la même démarche méthodologique au niveau des langages que ce qui est classiquement fait au niveau des composants logiciels. En l'occurrence, nous utilisons le formalisme des grammaires attribuées pour tenter de répondre à la question suivante : comment peut-on créer de nouveaux langages par composition de langages réutilisables existants ? Nous tirons profit de leur traduction en algèbres de combinateurs fonctionnels pour définir des spécifications exécutables de langages dédiés (vus comme composants logiciels), plongés dans le langage fonctionnel pur Haskell. \' partir d'exemples significatifs d'extension et de réutilisation de langages dédiés (par stratification de ceux-ci, ou par changement de monade), nous proposons un typage de langages dédiés en vue de leur assemblage et leur réutilisation. Pour illustrer cette démarche, nous décrivons un langage dédié (bibliothèque de combinateurs) pour l'édition de documents structurés. Un document y est représenté par un zipper attribué, une structure arborescente localisable, représentant un arbre et son contexte, et caractérisée par une grammaire attribuée. L'édition consiste alors à la modification interactive de cette structure ; ce qui entraîne une réévaluation totale ou partielle des attributs. L'édition peut aussi être réalisée à travers une vue abstraite obtenue par projection de la structure concrète. Ce qui pose le problème de \textit, un problème familier de la communauté des bases de données, auquel nous donnons une solution grâce à nos combinateurs d'éditeurs.

Le document traite du raisonnement sur les processus. Les chapitres principaux sont: - Équivalences comportementales : caractérisation logique, axiomatisation et congruence - Inspections et équivalences intensionnelles - Calculs avec localités