L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type. / Formal methods are rapidly improving and gaining ground in software. Type systems are the most successful and popular formal method used to develop software. As the technology of type systems progresses, new needs and new opportunities appear. One of those needs is to ensure the faithfulness of the translation from source code to machine code, so that the properties you prove about the code you write also apply to the code you run. This thesis presents a compiler from a polymorphic higher-order functional language to typed assembly language, whose main property is that type preservation is verified statically, through type annotations on the compiler's code. Our compiler implements the essential code transformations for a higher-order functional language, namely a CPS conversion and closure conversion as well as a code generation. The thesis presents the details of the strongly typed intermediate representations and the constraints they set on the implementation of code transformations. Our goal is to guarantee type preservation with a minimum of type annotations, and without compromising readability and modularity of the code. This goal is already a reality for simple types, and we discuss the problems remaining for polymorphism, which still requires substantial extra work to satisfy the type checker.

Le compilateur de parties opératives Apollon qui est présenté dans cette thèse, génère automatiquement le dessin des masques de parties opératives de circuits VLSI de type microprocesseur à partir d'une description comportementale de niveau transfert de registres constituée d'un ensemble non ordonné d'instructions opératives. Une instruction opérative est formée d'un ensemble d'actions opératives dont le format est prédéfini (transferts - opérations unaires ou binaires et entrées-sorties) devant se dérouler en parallèle en au plus deux cycles opératifs. Un cycle opératif comprend 4 phases qui correspondent aux 4 phases d'exécution d'un transfert entre 2 registres. Apollon est basé sur un modèle dérivé de la partie opérative du MC68000. Ce modèle fournit à la fois: un modèle architectural: la partie opérative est formée d'un ensemble de sous parties opératives alignées à deux bus qui traversent tous les éléments d'une sous partie opérative; un modèle temporel: une opération prend 2 cycles, un transfert un seul; un modèle électrique: les bus sont complémentés et à précharge; un modèle topologique: le plan de masse est basé sur la structure en tranches appelée communément bis slice. Le compilateur génère d'abord l'architecture de la partie opérative, puis les spécification des masques à partir de cette architecture. Pour générer l'architecture de la partie opérative en un temps raisonnable, le compilateur doit recourir à des heuristiques. Pour générer le dessin des masques, le compilateur utilise l'assembleur de silicium Lubrick qui permet d'assembler et de connecter automatiquement les cellules de base des éléments fonctionnels de la partie opérative. Les spécifications des masques sont générées à partir des spécifications des cellules prédéfinies d'une bibliothèque NMOS.

Cette thèse présente des contributions dans les domaines de l'architecture des ordinateurs réalisés sous la forme d'un Circuit Intégré. Un assembleur de silicium, appelé LUBRICK, permet de décrire, dans un langage de programmation, la constitution d'un assemblage hiérarchisé de cellules pour réaliser la description complète des masques d'un Circuit Intégré. La compilation du silicium, discipline qui consiste à déduire les masques d'un circuit en partant d'une description fonctionnelle, est ici abordée sous un angle pratique, avec la présentation d'un compilateur prototype d'une forme de partie contrôle et des présentations de modèles topologiques de parties opératives et de parties contrôle qui servent de cible au compilateur

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type. / Formal methods are rapidly improving and gaining ground in software. Type systems are the most successful and popular formal method used to develop software. As the technology of type systems progresses, new needs and new opportunities appear. One of those needs is to ensure the faithfulness of the translation from source code to machine code, so that the properties you prove about the code you write also apply to the code you run. This thesis presents a compiler from a polymorphic higher-order functional language to typed assembly language, whose main property is that type preservation is verified statically, through type annotations on the compiler's code. Our compiler implements the essential code transformations for a higher-order functional language, namely a CPS conversion and closure conversion as well as a code generation. The thesis presents the details of the strongly typed intermediate representations and the constraints they set on the implementation of code transformations. Our goal is to guarantee type preservation with a minimum of type annotations, and without compromising readability and modularity of the code. This goal is already a reality for simple types, and we discuss the problems remaining for polymorphism, which still requires substantial extra work to satisfy the type checker.