Cette thèse se place dans le cadre des méthodes formelles et plus précisément dans celui de la vérification déductive et du système Why3. Ce dernier fournit un ensemble d'outils pour la spécification, l'implémentation et la vérification à l'aide de démonstrateurs externes. Why3 propose en particulier un langage de programmation adapté à la preuve, appelé WhyML. Un aspect important de ce langage est le code fantôme, à savoir des éléments de programme introduits exclusivement pour les besoins de la spécification et de la preuve. Pour obtenir un code exécutable, le code fantôme est éliminé par un processus automatique appelé extraction. L'une des contributions principales de cette thèse est la formalisation et l'implémentation du mécanisme d'extraction deWhy3. La formalisation consiste à montrer que le programme extrait préserve la sémantique du programme de départ, en s'appuyant notamment sur un système de types avec effets. Ce mécanisme d'extraction a été utilisé avec succès pour obtenir plusieurs modules OCaml corrects par construction, dans le cadre d'une bibliothèque vérifiée de structures de données et d'algorithmes. Cet effort de preuve a conduit à deux autres contributions de cette thèse.La première est une technique systématique pour la vérification de structures avec pointeurs, à l'aide de modèles du tas délimités.Une preuve entièrement automatique d'une structure union-find a pu être obtenue grâce à cette technique. La seconde contribution est un moyen de spécifier un algorithme d'itération indépendamment de son implémentation. Plusieurs curseurs et itérateurs d'ordre supérieur ont été spécifiés et vérifiés en utilisant cette approche. / This thesis is set in the field of formal methods, more precisely in the domain of deductive program verification. Our working context is the Why3 framework, a set of tools to implement, formally specify, and prove programs usingoff-the-shelf theorem provers. Why3 features a programming language,called WhyML, designed with verification in mind. An important feature of WhyML is ghost code: portions of the program that are introduced for the sole purpose of specification andverification. When it comes to get an executable implementation, ghost code is removed by an automatic process called extraction. One of the main contributions of this thesis is the formalization and implementation of Why3's extraction. The formalization consists in showing that the extracted program preserves the same operational behavior as the original source code, based on a type and effect system. The new extraction mechanism has been successfully used to get correct-by-construction OCaml modules, which are part of averified OCaml library of data structures and algorithms. This verification effort led to two other contributions of this thesis.The first is a systematic approach to the verification ofpointer-based data structures using ghost models of fragments of the heap. A fully automatic verification of a union-find data structure was achieved using this technique. The second contribution is a modular way to reason about iteration, independently of the underlying implementation. Several cursors and higher-orderiterators have been specified and verified with this approach.

OCaml est un langage fonctionnel statiquement typé, qui génère après inférence de types un arbre de syntaxe abstraite dans lequel chacun des noeuds est annoté avec un ensemble d’informations issues de cette inférence. Ces informations, en particulier les types inférés, constituent une preuve de typage de l’expression annotée.Ce manuscrit de thèse s’intéresse à la vérification de ces arbres annotés en les considérant comme des preuves de typages du programme, et décrit un ensemble de règles permettant d’en vérifier la cohérence. La formalisation de ces règles de vérification de preuves de types peut être vue comme une représensation du système de types du langage étudié.Cette thèse présente plusieurs aspects de la vérification d’arbres de syntaxe annotés. Le premier cas étudié est la formalisation d’un dérivé de MiniML où toutes les expressions sont annotées de manière théoriquement parfaite, et montre qu’il est possible d’écrire des règles de vérification de manière algorithmique, rendant directe la preuve de correction vis-à-vis de la spécification. La seconde partie s’intéresse à la formalisation de règles de vérification pour un sous-ensemble du premier langage intermédiaire d’OCaml, le TypedTree, accompagné d’un vérificateur implémentant ces règles. Ces règles constituent alors une représentation du système de types d’OCaml, document jusqu’alors inexistant, au mieux disséminé dans diverses publications. / OCaml is a statically typed programming language that generates typed annotated abstract syntax trees after type inference. Each of their nodes contains information derived from the inference like the inferred type and the environment used to find this information. These annotated trees can then be seen as typing proofs of the program.In this thesis, we introduce a consistency checking of type-annotated trees, considering them as typing proof, and we describe a set of rules that defines the consistency property.Such consistency checking rules can then be seen as a formalized representation of the type system, since consistency ensures the typing invariants of the language.This thesis introduces multiple aspects of checking type-annotated trees. First of all, it considers a simplified and ideal version of MiniML and formalizes a set of rules to check consistency. In this formalism, we consider ideally type-annotated trees, which might not be the case for OCaml typed trees. Such type checking rules are presented in an algorithmic form, reducing as much as possible the gap from formalism to implementation. As such, they ease the correction proof between the implementation of the type checker and the specification of the type system. The second part of this thesis is dedicated to the formalization of a set of rules for a subset of the OCaml annotated trees: the TypedTree. The formalism described in these chapters is implemented as a type checker working on large subset of the language, leaving the formalization of some aspects for a further work. These rules constitute a formalized representation of the OCaml type system in a single document.

Établir des preuves de bon fonctionnement des programmes est délicat ; on a recours à des outils de preuve, qui doivent procéder par surapproximation (à cause du théorème de Rice). La complétion d'automate est un tel outil, qui surapproxime l'ensemble des termes accessibles lors de l'exécution d'un programme représenté par un système de réécriture. La stratégie d'évaluation donne l'ordre dans lequel les sous-termes d'un terme doivent être réécrits ; en tenir compte permet une meilleur précision de l'analyse. Notre thèse propose une adaptation de la complétion d'automate à la stratégie en profondeur, utilisée notamment par OCaml. Nous établissons la correction et la précision de notre méthode et montrons comment elle s'inscrit dans le cadre plus large de l'analyse de programmes fonctionnels (OCaml). / Proving that programs behave correctly is difficult; one uses proof tools, which must rely on overapproximation (because of Rice's theorem). Automaton completion is such a tool, which overapproximates the set of reachable terms during the execution of a program represented as a TRS. An evaluation strategy dictates which subterm of a term should be rewritten first; taking this into account allows for a better approximation. Our thesis sets forward an adaptation of automaton completion to the innermost strategy, which is used among others by OCaml. We prove the soundness and the precision of our adaptation and show how it is part of a greater framework for analysis of functional programms (OCaml).

The increasing commoditization of computers in modern society has exceeded the pace of associated developments in reliability. Although theoretical computer science has advanced greatly in the last thirty years, many of the best techniques have yet to find their way into embedded computers, and their failure can have a great potential for disrupting society. This dissertation presents some approaches to improve computer reliability using software and hardware techniques, and makes the following claims for novelty: innovative development of a toolchain and libraries to support extraction from dependent type checking in a theorem prover; conceptual design and deployment in reconfigurable hardware; an extension of static type-safety to hardware description language and FPGA level; elimination of legacy C code from the target and toolchain; a novel hardware error detection scheme is described and compared with conventional triple modular redundancy. The elimination of any user control of memory management promotes robustness against buffer overruns, and consequently prevents vulnerability to common Trojan techniques. The methodology identifies type punning as a key weakness of commonly encountered embedded languages such as C, in particular the extreme difficulty of determining if an array access is in bounds, or if dynamic memory has been properly allocated and released. A method of eliminating dependence on type-unsafe libraries is presented, in conjunction with code that has optionally been proved correct according to user-defined criteria. An appropriately defined subset of OCaml is chosen with support for the Coq theorem prover in mind, and then evaluated with a custom backend that supports behavioural Verilog, as well as a fixed execution unit and associated control store. Results are presented for this alternative platform for reliable embedded systems development that may be used in future industrial flows. To provide assurance of correct operation, the proven software needs to be executed in an environment where errors are checked and corrected in conjunction with appropriate exception processing in the event of an uncorrectable error. Therefore, the present author’s previously published error detection scheme based on dual-rail logic and self-checking checkers is further developed and compared with traditional N-modular redundancy.

Le typage statique des langages de programmation garantit des propriétés de sûreté d'exécution des programmes et permet l'usage de représentations de données dénuées d'informations de types. En présence de primitives de (dé)sérialisation, ces données brutes peuvent invalider les propriétés apportées par le typage statique. Il est alors utile de pouvoir tester dynamiquement la compatibilité des données lues avec le type statique attendu. Cette thèse définit, dans le cadre des langages de programmation basés sur un système de types avec polymorphisme paramétrique et utilisant une représentation uniforme des données, une notion de compatibilité d'un graphe mémoire (désérialisé) avec un type ; cette notion s'exprime sous la forme de contraintes de types sur les nœuds du graphe mémoire. Cette formalisation permet de construire un mécanisme de résolution de contraintes par réécriture, puis un algorithme de vérification de compatibilité d'un graphe mémoire avec un type. Les propriétés de correction et de complétude de l'algorithme obtenu sont étudiées en présence de types algébriques, de données modifiables, de cycles et de valeurs fonctionnelles. Cette thèse propose également un prototype pour le compilateur OCaml.

Programmer en un langage de programmation peut être une tâche ardue. Même les plus chevronnés ne sont pas à l’abri de commettre des erreurs. Il est donc important pour les programmeurs d’avoir des aides pour écrire leur code plus efficacement et plus rapidement. Typer est un jeune langage de programmation en développement. Actuellement, le langage a beaucoup de limitations d’aides pour les programmeurs. En effet, on ne peut coder en Typer que dans un terminal, dans un fichier et compiler le fichier ou dans des environnements primitifs. On apporte une solution à ce problème en offrant, dans ce travail, un serveur LSP au langage qui va offrir des fonctionnalités comme la complétion de code, le surlignement des erreurs, etc, pour permettre aux programmeurs Typer de coder plus facilement et de pouvoir le faire dans leur éditeur/IDE préféré. / Programming in a programming language can be a daunting task. Even the most seasoned are not immune to make mistakes. It is therefore important for programmers to have helpers to write their code more efficiently and quickly. Typer is a young programming language in development. Currently, the language has a lot of helper limitations for programmers. Indeed, we can code in Typer only in a terminal, in a file and compile the file or in primitive environments. We solve this problem by offering in this work, an LSP server to the language which will offer features such as code completion, error highlighting...etc, to allow Typer programmers to code more easily and efficiently, and also, to be able to do it in their favorite editor/IDE.

<p dir="ltr">Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. When that language is sufficiently similar to that of the proof assistant, one solution is to use a <i>shallow embedding</i> to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present <i>GSet</i>, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the translation algorithm between GADTml and gCIC, together with a proof of the soundness of this translation. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.</p>

Cette thèse traite des simulations multidomaines des écoulements en milieu poreux. Trois aspects sont abordés. Une étude est d'abord menée concernant une méthode de décomposition de domaines avec des maillages non-raccordés, utilisant des conditions d'interface de type Robin, pour les éléments finis mixtes. D'autre part, la méthode est implémentée en parallèle à l'aide du système parallèle OcamlP3l, écrit par des informaticiens dans le langage Ocaml. En OcamlP3l, l'utilisateur programme et débogue en séquentiel, puis obtient le code parallèle par une simple recompilation. Enfin, nous présentons un nouveau modèle d'écoulement dans un mileu poreux contenant de grandes fractures, avec des perméabilités très grandes et/ou très faibles. Dans ce modèle, les fractures sont traitées comme des interfaces entre sous-domaines. Une analyse théorique prouve l'existence et l'unicité de la solution, fournit une estimation d'erreur, qui est confirmée par des tests numériques.

Le but de cette thèse est d'étudier la somme et le zéro dans deux principaux cadres : les isomorphismes de types et la normalisation de lambda-termes. Les isomorphismes de type avaient déjà été étudiés dans le cadre du lambda-calcul simplement typé avec paires surjectives mais sans somme. Pour aborder le cas avec somme et zéro, j'ai commencé par restreindre l'étude au cas des isomorphismes linéaires, dans le cadre de la logique linéaire, ce qui a conduit à une caractérisation remarquablement simple de ces isomorphismes, obtenue grâce à une méthode syntaxique sur les réseaux de preuve. Le cadre plus général de la logique intuitionniste correspond au problème ouvert de la caractérisation des isomorphismes dans les catégories bi-cartésiennes fermées. J'ai pu apporter une contribution à cette étude en montrant qu'il n'y a pas d'axiomatisation finie de ces isomorphismes. Pour cela, j'ai tiré partie de travaux en théorie des nombres portant sur un problème énoncé par Alfred Tarski et connu sous le nom du « problème des égalités du lycée ». Pendant tout ce travail sur les isomorphismes de types, s'est posé le problème de trouver une forme canonique pour représenter les lambda-termes, que ce soit dans le but de nier l'existence d'un isomorphisme par une étude de cas sur la forme du terme, ou pour vérifier leur existence dans le cas des fonctions très complexes que j'étais amené à manipuler. Cette réflexion a abouti à poser une définition « extensionnelle » de forme normale pour le lambda-calcul avec somme et zéro, obtenue par des méthodes catégoriques grâce aux relations logiques de Grothendieck, apportant ainsi une nouvelle avancée dans l'étude de la question réputée difficile de la normalisation de ce lambda-calcul. Enfin je montrerai comment il est possible d'obtenir une version « intentionnelle » de ce résultat en utilisant la normalisation par évaluation. J'ai pu ainsi donner une adaptation de la technique d' évaluation partielle dirigée par les types pour qu'elle produise un résultat dans cette forme normale, ce qui en réduit considérablement la taille et diminue aussi beaucoup le temps de normalisation dans le cas des isomorphismes de types considérés auparavant.