A Type-Preserving Compiler from System F to Typed Assembly Language

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.

A Compiler for the dependently typed language Beluga

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage.

The adoption of advanced feed-in tariffs in Ontario : a case of institutional layering

En mai 2009, l’Ontario a adopté la Loi sur l’énergie verte et devint ainsi la première juridiction en Amérique du Nord à promouvoir l’énergie renouvelable par le biais de tarifs de rachat garantis. En novembre 2010, dans son Plan énergétique à long terme, la province s’est engagée à déployer 10,700 MW en capacité de production d’énergie renouvelable non-hydroélectrique par 2018. Il s’agit de la cible de déploiement la plus élevée dans ce secteur au Canada. Les infrastructures de production et de distribution d’électricité comprennent des coûts d’installation élevés, une faible rotation des investissements et de longs cycles de vie, facteurs qui servent habituellement à ancrer les politiques énergétiques dans une dynamique de dépendance au sentier. Depuis le début des années 2000, cependant, l’Ontario a commencé à diverger de sa traditionnelle dépendance aux grandes centrales hydroélectriques, aux centrales à charbon et aux centrales nucléaires par une série de petits changements graduels qui feront grimper la part d’énergie renouvelable dans le mix énergétique provincial à 15% par 2018. Le but de ce mémoire est d’élucider le mécanisme de causalité qui a sous-tendu l’évolution graduelle de l’Ontario vers la promotion de l’énergie renouvelable par le biais de tarifs de rachat garantis et d’une cible de déploiement élevée. Ce mémoire applique la théorie du changement institutionnel graduel de Mahoney et Thelen au cas du développement de politiques d’énergie renouvelable en Ontario afin de mieux comprendre les causes, les modes et les effets du changement institutionnel. Nous découvrons que le contexte canadien de la politique énergétique favorise la sédimentation institutionnelle, c’est-à-dire un mode changement caractérisé par de petits gains favorisant l’énergie renouvelable. Ces gains s’accumulent pourtant en transformation politique importante. En Ontario, la mise sur pied d’une vaste coalition pour l’énergie renouvelable fut à l’origine du changement. Les premiers revendicateurs de politiques favorisant l’énergie renouvelable – les environnementalistes et les premières entreprises d’approvisionnement et de service en technologies d’énergie renouvelable – ont dû mettre sur pied un vaste réseau d’appui, représentant la quasi-totalité de la société ontarienne, pour faire avancer leur cause. Ce réseau a fait pression sur le gouvernement provincial et, en tant que front commun, a revendiqué l’énergie renouvelable non seulement comme solution aux changements climatiques, mais aussi comme solution à maints autres défis pressants de santé publique et de développement économique. La convergence favorable d’un nombre de facteurs contextuels a certes contribué à la réussite du réseau ontarien pour l’énergie renouvelable. Cependant, le fait que ce réseau ait trouvé des alliés au sein de l’exécutif du gouvernement provincial s’est révélé d’importance cruciale quant à l’obtention de politiques favorisant l’énergie renouvelable. Au Canada, les gouvernements provinciaux détiennent l’ultime droit de veto sur la politique énergétique. Ce n’est qu’en trouvant des alliés aux plus hauts échelons du gouvernement que le réseau ontarien pour l’énergie renouvelable a pu réussir.

End-of-Life Decisions and Advanced Old Age

Article

Abitbol : un langage sur mesure pour la métaprogrammation

Ce mémoire a pour thèse que les fonctions devraient être transparentes lors de la phase de métaprogrammation. En effet, la métaprogrammation se veut une possibilité pour le programmeur d’étendre le compilateur. Or, dans un style de programmation fonctionnelle, la logique du programme se retrouve dans les définitions des diverses fonctions le composant. Puisque les fonctions sont généralement opaques, l’impossibilité d’accéder à cette logique limite les applications possibles de la phase de métaprogrammation. Nous allons illustrer les avantages que procurent les fonctions transparentes pour la métaprogrammation. Nous donnerons notamment l’exemple du calcul symbolique et un exemple de nouvelles optimisations désormais possibles. Nous illustrerons également que la transparence des fonctions permet de faire le pont entre les datatypes du programme et les fonctions. Nous allons également étudier ce qu'implique la présence de fonctions transparentes au sein d'un langage. Nous nous concentrerons sur les aspects reliés à l'implantation de ces dernières, aux performances et à la facilité d'utilisation. Nous illustrerons nos propos avec le langage Abitbol, un langage créé sur mesure pour la métaprogrammation.