Search

While folklore teaches us that closures and objects are two sides of the same coin, they remain quite different in practice, most notably because closures are opaque, the only supported operation being to call them. In this article we discuss a few cases where we need functions to be less opaque, and propose to satisfy this need by extending our beloved λ so as to expose as sorts of record fields some of the variables it captures. These open closures are close relatives of CLOS's funcallable objects as well as of the function objects of traditional object-oriented languages like Java, except that they are functions made to behave like objects rather than the reverse. We present the design and implementation of such a feature in the context of Emacs Lisp.

Of all the threats to the consistency of a type system, such as side effects and recursion, impredicativity is arguably the least understood. In this paper, we try to investigate it using a kind of blackbox reverse-engineering approach to map the landscape. We look at it with a particular focus on its interaction with the notion of implicit arguments, also known as erasable arguments. More specifically, we revisit several famous type systems believed to be consistent and which do include some form of impredicativity, and show that they can be refined to equivalent systems where impredicative quantification can be marked as erasable, in a stricter sense than the kind of proof irrelevance notion used for example for Prop terms in systems like Coq. We hope these observations will lead to a better understanding of why and when impredicativity can be sound. As a first step in this direction, we discuss how these results suggest some extensions of existing systems where constraining impredicativity to erasable quantifications might help preserve consistency.

When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effort. In this paper, we show how Beluga's dependent contextual types let us use higher-order abstract syntax (HOAS) to implement a type-preserving compiler for the simply-typed lambda-calculus, including transformations such as closure conversion and hoisting. Unlike previous implementations, which have to abandon HOAS locally in favor of a first-order binder representation, we are able to take advantage of HOAS throughout the compiler pipeline, so that the compiler code stays clean and we do not need extra lemmas about binder manipulation. Our work demonstrates that HOAS encodings offer substantial benefits to certified programming. Scope and type safety of the code transformations are statically guaranteed, and our implementation nicely mirrors the paper proof of type preservation, and can hence be seen as an encoding of the proof which happens to be executable as well., Journal of Formalized Reasoning, Vol 8, No 1 (2015)

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.

On est habitué à penser comme suit à un programme qui exécute: une donnée entre (un input), un moment passe, et un résultat ressort. On assume tacitement de l'information complète sur le input, le résultat, et n'importe quels résultats intermédiaires. Dans ce travail-ci, on demande ce que ça voudrait dire d'exécuter un programme sur de l'information partielle. Comme réponse possible, on introduit l'interprétation partielle, notre contribution principale. Au lieu de considérer un seul input, on considère un ensemble de inputs possibles. Au lieu de calculer un seul résultat, on calcule un ensemble de résultats possibles, et des ensembles de résultats intermédiaires possibles. On approche l'interprétation partielle à partir du problème de la spécialisation de programme: l'optimisation d'un programme pour certains inputs. Faire ça automatiquement porte historiquement le nom d'évaluation partielle. Ç'a été appliqué avec succès à plusieurs problèmes spécifiques. On croit que ça devrait être un outil de programmation commun, pour spécialiser des librairies générales pour usage spécifique - mais ce n'est pas le cas. Souvent, une implantation donnée de l'évaluation partielle ne fonctionne pas uniformément bien sur tous les programmes. Ça se prête mal à un usage commun. On voit ce manque de régularité comme un problème de précision: si l'évaluateur partiel était très précis, il trouverait la bonne spécialisation, indépendamment de notre style de programme. On propose donc une approche de principe à l'évaluation partielle, visant la précision complète, retirée d'exemples particuliers. On reformule l'évaluation partielle pour la baser sur l'interprétation partielle: le calcul sur de l'information partielle. Si on peut déterminer ce qu'on sait sur chaque donnée dans le programme, on peut décider quelles opérations peuvent être éliminées pour spécialiser le programme: les opérations dont le résultat est unique. On définit une représentation d'ensembles qui ressemble à la définition en compréhension, en mathématiques. On modifie un interpréteur pour des programmes fonctionnels, pour qu'il calcule sur ces ensembles. On utilise un solver SMT pour réaliser les opérations sur les ensembles. Pour assurer la terminaison de l'interpréteur modifié, on applique des idées de l'interprétation abstraite: le calcul de point fixe, et le widening. Notre implantation initiale produit de bons résultats, mais elle est lente pour de plus gros exemples. On montre comment l'accélérer mille fois, en dépendant moins de SMT., We are used to the following picture of an executing program: an input is provided, the program runs for a while, and a result comes out. We tacitly assume complete information about the input, the result, and any intermediate results in between. In this work, we ask what it would mean to execute a program over partial information. As a possible answer, we introduce partial interpretation, our main contribution. Instead of considering a unique input, we consider a set of possible inputs. Instead of computing a unique result, we compute a set of possible results, and sets of possible intermediate results. We approach partial interpretation from the problem of program specialization: the optimization of a program's execution time for certain inputs. Doing this automatically is historically known as partial evaluation. Partial evaluation has been applied successfully to many specific problems. We believe it should be a mainstream programming tool, to specialize general libraries for specific use - but such a tool has not been delivered. One common problem is that a given implementation of partial evaluation is inconsistent: it does not work uniformly well on all input programs. This inconsistency makes it unsuited for mainstream use. We view this inconsistency as an accuracy problem: if the partial evaluator was very accurate, it would find the correct specialization, no matter how we present the input program. We therefore propose a principled approach to partial evaluation, aimed at complete accuracy, removed from any particular example program. We reformulate partial evaluation to root it in partial interpretation: computation over partial information. If we can determine what we know about every piece of data in the program, we can decide which operations can be removed to specialize the program: those operations whose result is uniquely known. We represent sets with a kind of mathematical set comprehension. We modify an interpreter for functional programs, to compute over these sets. We use an SMT solver (Satisfiability Modulo Theories) to perform set operations. To ensure termination of the modified interpreter, we apply ideas from abstract interpretation: fixed point computation, and widening. Our initial implementation produces good results, but it is slow for larger examples. We show how to speed it up a thousandfold, by relying less on SMT.

La modularité est un enjeu important en programmation, surtout quand on l’enrichit avec des preuves, comme dans les langages avec des types dépendants. Typer est un tel langage, et afin d’augmenter sa modularité et de lui ajouter un moyen de faire la surcharge d’opérateurs, on s’inspire d’Agda et Coq et on l’étend avec les arguments instances, qui généralisent les classes de types de Haskell. Un aspect qui distingue notre conception est que comme Typer généralise les définitions, la généralisation des contraintes de classe est grandement facilitée. Pour pouvoir faire les preuves de lois de classes, on doit également ajouter l’élimination dépendante des types inductifs au langage, dont certains aspects sont en retour facilités par les arguments instances. Sur la base de ces deux fonctionnalités, on offre également une solution au problème de la cécité booléenne, tel que décrit par Harper., Modularity is an important concern for software development, especially when the latter is enriched with proofs in a language with dependent types. Typer is such a language, and in order to increase its modularity, and also provide a way to overload operators, we take inspiration from Agda and Coq and extend it with instance arguments, a generalization of Haskell’s type classes. An aspect that sets our design apart is that since Typer generalizes definitions, it greatly simplifies the generalization of class constraints. In order to allow writing proofs for class laws, we must also implement the dependent elimination of inductive types. In return, instance arguments facilitate some details of dependent elimination. Using both features, we suggest a solution to the problem of Boolean Blindness.

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., Our main thesis is that functions should be transparent during the metaprogramming stage. Metaprogramming is intended as a possibility for the programmer to extend the compiler. But in a functional programming style, the program logic is found in the definition of its functions. Since functions are generally opaque, it is impossible for the programmer to access this information and this limits the metaprogramming possibilities. We will illustrate the benefits of transparent functions for metaprogramming. We will give the example of symbolic computation and also show new forms of optimizations now available at the metaprogramming stage. We will also illustrate that transparency allows us to bridge the gap between the datatypes of a program and its functions. We will also examine how transparent functions affects other aspects of the language. We will focus on how to implement them, their performance impact and their ease of use. We illustrate our thesis with Abitbol, a language designed for metaprogramming.

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., In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system. In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time. Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga.

La conception de systèmes hétérogènes exige deux étapes importantes, à savoir : la modélisation et la simulation. Habituellement, des simulateurs sont reliés et synchronisés en employant un bus de co-simulation. Les approches courantes ont beaucoup d’inconvénients : elles ne sont pas toujours adaptées aux environnements distribués, le temps d’exécution de simulation peut être très décevant, et chaque simulateur a son propre noyau de simulation. Nous proposons une nouvelle approche qui consiste au développement d’un simulateur compilé multi-langage où chaque modèle peut être décrit en employant différents langages de modélisation tel que SystemC, ESyS.Net ou autres. Chaque modèle contient généralement des modules et des moyens de communications entre eux. Les modules décrivent des fonctionnalités propres à un système souhaité. Leur description est réalisée en utilisant la programmation orientée objet et peut être décrite en utilisant une syntaxe que l’utilisateur aura choisie. Nous proposons ainsi une séparation entre le langage de modélisation et la simulation. Les modèles sont transformés en une même représentation interne qui pourrait être vue comme ensemble d’objets. Notre environnement compile les objets internes en produisant un code unifié au lieu d’utiliser plusieurs langages de modélisation qui ajoutent beaucoup de mécanismes de communications et des informations supplémentaires. Les optimisations peuvent inclure différents mécanismes tels que le regroupement des processus en un seul processus séquentiel tout en respectant la sémantique des modèles. Nous utiliserons deux niveaux d’abstraction soit le « register transfer level » (RTL) et le « transaction level modeling » (TLM). Le RTL permet une modélisation à bas niveau d’abstraction et la communication entre les modules se fait à l’aide de signaux et des signalisations. Le TLM est une modélisation d’une communication transactionnelle à un plus haut niveau d’abstraction. Notre objectif est de supporter ces deux types de simulation, mais en laissant à l’usager le choix du langage de modélisation. De même, nous proposons d’utiliser un seul noyau au lieu de plusieurs et d’enlever le bus de co-simulation pour accélérer le temps de simulation., The design of heterogeneous systems requires two main steps, modeling and simulation. Usually, simulators are connected and synchronized by using a cosimulation bus. These current approaches have many disadvantages: they are not always adapted to the distributed environments, the execution time can be very disappointing, and each simulator has its own core of simulation. We propose a new approach which consists in developing a multi-language compiled simulator where each model can be described by employing various modeling languages such as SystemC, ESyS.Net or others. Each model contains modules and communication links between them. These modules describe functionalities for a desired system. Their description is realized by using the programming object and can be described by using a syntax that a user will have chosen. We thus propose a separation between the language of modeling and simulation. The models are transformed into the same internal representation which could be seen like unique objects. Our environment compiles these internal objects by producing a unified code instead of using several languages of modeling which add many mechanisms of communications and extra informations. Optimizations can include various mechanisms such as merging processes into only one sequential process while respecting the semantics of the models. We will use two abstraction levels, the “register transfer level”(RTL) and the “transaction-level modeling”(TLM). RTL allows a low level abstraction for modeling and the communication between the modules is done with signals. The TLM is a modeling for transactional communication with a higher abstraction level than RTL. Our aim is to support these two types of simulation, but the user can choose the language of modeling. In the same way, we propose to use a single core and to remove the cosimulation bus to accelerate the simulation time.

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.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.