A Type-Preserving Compiler from System F to Typed Assembly Language
Thèse ou mémoire / Thesis or Dissertation
Date de publication
Autrices et auteurs
Identifiant ORCID de l’auteur
Contributrices et contributeurs
Direction de recherche
Publié dans
Date de la Conférence
Lieu de la Conférence
Éditeur
Cycle d'études
Doctorat / Doctoral
Programme
Affiliation
Mots-clés
- Compilation certifiée
- Certified compilation
- Langage assembleur typé
- Typed assembly language
- Polymorphisme
- Polymorphism
- Vérification formelle
- Program verification
- Liaisons
- Bindings
Organisme subventionnaire
Résumé
Résumé
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.
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.
Table des matières
Notes
Notes
Autre version linguistique
Ensemble de données lié
Licence
Approbation
Évaluation
Complété par
Référencé par
Ce document diffusé sur Papyrus est la propriété exclusive des titulaires des droits d'auteur et est protégé par la Loi sur le droit d'auteur (L.R.C. (1985), ch. C-42). Sauf si le document est diffusé sous une licence Creative Commons, il ne peut être utilisé que dans le cadre d'une utilisation équitable et non commerciale comme le prévoit la Loi (i.e. à des fins d'étude privée ou de recherche, de critique ou de compte-rendu). Pour toute autre utilisation, une autorisation écrite des titulaires des droits d'auteur sera nécessaire.