Par "approche langage" on entend désigner une approche qui s'exprime, soit dans un langage de programmation, soit par un langage de programmation.<br />Les approches qui s'expriment dans le langage ne font appel à aucun formalisme éloigné (e.g. sémantique). Le langage de programmation est l'unique cadre de travail pour exprimer le problème, le résoudre et appliquer la solution. Nous montrons :<br /><br />- comment la compilation des langages fonctionnels peut s'exprimer dans le langage lui-même par transformation de programme. Ce cadre unifié permet de décrire, prouver, comparer et classifier la plupart des mises en œuvre de langages fonctionnels,<br /><br />- deux optimisations de l'implémentation des langages fonctionnels (une analyse de globalisation et un GC étendu) qui reposent sur la syntaxe et le type des expressions.<br /><br /><br /> Pour les approches qui s'expriment par un langage de programmation, il s'agit de prévenir le problème ou d'assurer une propriété via l'utilisation d'un langage (ou d'une discipline de programmation). Nous illustrons ce style d'approche par trois exemples :<br /><br /><br />- les types graphes qui permettent de définir et vérifier le partage des structures de données à pointeurs,<br /><br />- un langage dédié au parallélisme qui garantit une analyse de coût précise et un choix automatique de la meilleure distribution,<br /><br />- un style de programmation par aspects qui permet d'imposer automatiquement des propriétés aux programmes.

Nous nous intéressons ici à la génération de programmes certifiés<br />corrects par construction. Ces programmes sont obtenus en<br />extrayant l'information pertinente de preuves constructives réalisées<br />dans l'assistant de preuves Coq.<br /><br />Une telle traduction, ou "extraction", des preuves constructives<br />en programmes fonctionnels n'est pas nouvelle, elle correspond <br />à un isomorphisme bien connu sous le nom de Curry-Howard. Et<br />l'assistant Coq comporte depuis longtemps un tel outil d'extraction. <br />Mais l'outil précédent présentait d'importantes limitations. Certaines <br />preuves Coq étaient ainsi hors de son champ d'application, alors que <br />d'autres engendraient des programmes incorrects.<br /><br />Afin de résoudre ces limitations, nous avons effectué une refonte<br />complète de l'extraction dans Coq, tant du point de vue de la théorie<br />que de l'implantation. Au niveau théorique, cette refonte a entraîné<br />la réalisation de nouvelles preuves de correction de ce mécanisme<br />d'extraction, preuves à la fois complexes et originales. Concernant<br />l'implantation, nous nous sommes efforcés d'engendrer du code <br />extrait efficace et réaliste, pouvant en particulier être intégré dans des<br />développement logiciels de plus grande échelle, par le biais de<br />modules et d'interfaces.<br /><br />Enfin, nous présentons également plusieurs études de cas illustrant<br />les possibilités de notre nouvelle extraction. Nous décrivons ainsi la<br />certification d'une bibliothèque modulaire d'ensembles finis, et <br />l'obtention de programmes d'arithmétique réelle exacte à partir d'une <br />formalisation d'analyse réelle constructive. Même si des progrès <br />restent encore à obtenir, surtout dans ce dernier cas, ces exemples <br />mettent en évidence le chemin déjà parcouru.

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

Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées / Finding a good paradigm to represent parallel programming in a simple and efficient way is a challenge currently faced by computer science research, mainly due to the evolution of machine architectures towards multi-core processors. BSML is a high level, structured parallel programming language that takes part in the research in an original way. By building upon existing work, this thesis extends the language and makes it more general, simple and usable with added imperative features such as references and exceptions, a specific syntax, etc. The existing formal and safety characteristics of the language (semantics, type system...) are preserved and extended. A major application is given in the form of a methodology for the development of fully proved parallel programs

Ce manuscrit présente une méthode de conception au niveau système reposant sur la programmation fonctionnelle typée et visant à atténuer certains des problèmes complexifiant le développement des systèmes numériques modernes, tels que leurs tailles importantes ou la grande variété des blocs les constituant. Nous proposons un ensemble de mécanismes permettant de mélanger au sein d'un même design plusieurs formalismes de description distincts («modèles de calcul») se situant potentiellement à des niveaux d'abstraction différents. De plus, nous offrons au concepteur la possibilité d'expliciter directement les paramètres explorables de chaque sous-partie du design, puis d'en déterminer des valeurs acceptables via une étape d'exploration partiellement ou totalement automatisée réalisée à l'échelle du système. Les gains qu'apportent ces stratégies nouvelles sont illustrés sur plusieurs exemples. / This work presents a novel system-level design method based on typed functional programming and aiming at mitigating some of the issues making the development of modern digital systems complex, such as their increasing sizes and the variety of their subcomponents. We propose a range of mechanisms allowing to mix within a single design several description formalisms (``models of computation''), possibly at different abstraction levels. Moreover, the designer is provided with means to directly express the explorable parameters of each part of their design, and to find acceptable values for them through a partially or totally automatic system-wide architectural exploration step. The advantages brought by those new strategies are illustrated on several examples.

Ce mémoire décrit et évalue un système de module qui améliore la migration de code dans le langage de programmation distribuée Termite Scheme. Ce système de module a la possibilité d’être utilisé dans les applications qu’elles soient distribuées ou pas. Il a pour but de faciliter la conception des programmes dans une structure modulaire et faciliter la migration de code entre les nœuds d’un système distribué. Le système de module est conçu pour le système Gambit Scheme, un compilateur et interprète du langage Scheme utilisé pour implanter Termite. Le système Termite Scheme est utilisé pour implémenter les systèmes distribués. Le problème qui est résolu est la diffusion de code compilé entre les nœuds d’un système distribué quand le nœud destination n’a aucune connaissance préalable du code qu’il reçoit. Ce problème est difficile car les nœuds sont hétérogènes, ils ont différentes architectures (x86, ARM). Notre approche permet d’identifier les modules de façon unique dans un contexte dis- tribué. La facilité d’utilisation et la portabilité ont été des facteurs importants dans la conception du système de module. Le mémoire décrit la structure des modules, leur implémentation dans Gambit et leur application. Les qualités du système de module sont démontrées par des exemples et la performance est évaluée expérimentallement. / This thesis presents a module system for Termite Scheme that supports distributed computing. This module system facilitates application modularity and eases code migration between the nodes of a distributed system. This module system also works for developing non-distributed applications. The Gambit Scheme system is used to implement the distributed Termite and the Module system. The problem that is solved is the migration of compiled code between nodes of a distributed system when the receiving node has no prior knowledge of the code. This is a challenging problem because the nodes are not homogenous, they have different architectures (ARM, x86). Our approach uses a naming model for the modules that uniquely identifies them in a distributed context. Both ease of use and portability were important factors in the design of the module system. The thesis describes a module system and how it was integrated into Gambit. The system allows developing distributed modular systems. The features of this system are shown through application examples and the performance is evaluated experimentally.

Les questions de sûreté et d'incertitudes sont au centre des études de faisabilité pour un site de stockage souterrain de déchets nucléaires, en particulier l'évaluation des incertitudes sur les indicateurs de sûreté qui sont dues aux incertitudes sur les propriétés du sous-sol et des contaminants. L'approche globale par les méthodes probabilistes de type Monte Carlo fournit de bons résultats, mais elle demande un grand nombre de simulations. La méthode déterministe étudiée ici est complémentaire. Reposant sur la décomposition en valeurs singulières de la dérivée du modèle, elle ne donne qu'une information locale, mais elle est beaucoup moins coûteuse en temps de calcul. Le modèle d'écoulement suit la loi de Darcy et le transport des radionucléides autour du site de stockage est modélisé par une équation de diffusion-convection linéaire. Différentiation à la main et différentiation automatique sont comparées sur ces modèles en mode direct et en mode adjoint. Une étude comparée des deux approches probabiliste et déterministe pour l'analyse de la sensibilité des flux de contaminants aux exutoires par rapport aux variations des paramètres d'entrée est menée sur des données réalistes fournies par l'ANDRA. Des outils génériques d'analyse de sensibilité et de couplage de code sont développés en langage Caml. Ils permettent à l'utilisateur de ces plates-formes génériques de ne fournir que la partie spécifique de l'application dans le langage de son choix. Une étude sur les écoulements diphasiques eau/air partiellement saturés en hydrogéologie porte sur les limitations des approximations de Richards et de la formulation en pression globale issue du domaine pétrolier.

Thesis (Ph. D.)--Harvard University, 1985. / Includes bibliographical references (p).

Les outils de programmation sont des programmes informatiques qui aident les humains à programmer des ordinateurs. Les outils sont de toutes formes et tailles, par exemple les éditeurs, les compilateurs, les débogueurs et les profileurs. Chacun de ces outils facilite une tâche principale dans le flux de travail de programmation qui consomme des ressources cognitives lorsqu’il est effectué manuellement. Dans cette thèse, nous explorons plusieurs outils qui facilitent le processus de construction de systèmes intelligents et qui réduisent l’effort cognitif requis pour concevoir, développer, tester et déployer des systèmes logiciels intelligents. Tout d’abord, nous introduisons un environnement de développement intégré (EDI) pour la programmation d’applications Robot Operating System (ROS), appelé Hatchery (Chapter 2). Deuxièmement, nous décrivons Kotlin∇, un système de langage et de type pour la programmation différenciable, un paradigme émergent dans l’apprentissage automatique (Chapter 3). Troisièmement, nous proposons un nouvel algorithme pour tester automatiquement les programmes différenciables, en nous inspirant des techniques de tests contradictoires et métamorphiques (Chapter 4), et démontrons son efficacité empirique dans le cadre de la régression. Quatrièmement, nous explorons une infrastructure de conteneurs basée sur Docker, qui permet un déploiement reproductible des applications ROS sur la plateforme Duckietown (Chapter 5). Enfin, nous réfléchissons à l’état actuel des outils de programmation pour ces applications et spéculons à quoi pourrait ressembler la programmation de systèmes intelligents à l’avenir (Chapter 6). / Programming tools are computer programs which help humans program computers. Tools come in all shapes and forms, from editors and compilers to debuggers and profilers. Each of these tools facilitates a core task in the programming workflow which consumes cognitive resources when performed manually. In this thesis, we explore several tools that facilitate the process of building intelligent systems, and which reduce the cognitive effort required to design, develop, test and deploy intelligent software systems. First, we introduce an integrated development environment (IDE) for programming Robot Operating System (ROS) applications, called Hatchery (Chapter 2). Second, we describe Kotlin∇, a language and type system for differentiable programming, an emerging paradigm in machine learning (Chapter 3). Third, we propose a new algorithm for automatically testing differentiable programs, drawing inspiration from techniques in adversarial and metamorphic testing (Chapter 4), and demonstrate its empirical efficiency in the regression setting. Fourth, we explore a container infrastructure based on Docker, which enables reproducible deployment of ROS applications on the Duckietown platform (Chapter 5). Finally, we reflect on the current state of programming tools for these applications and speculate what intelligent systems programming might look like in the future (Chapter 6).