Our work applies the dataflow algorithm to an area outside its traditional scope: functional languages. Our approach relies on a monadic intermediate language that provides low-level, imperative features like computed jumps and explicit allocations, while at the same time supporting high-level, functional-language features like case discrimination and partial application. We prototyped our work in Haskell using the HOOPL library and this dissertation shows numerous examples demonstrating its use. We prove the efficacy of our approach by giving a novel description of the uncurrying optimization in terms of the dataflow algorithm, as well as a complete implementation of the optimization using HOOPL.

Due to the complex nature of parallel programming, it is difficult to diagnose and solve performance related problems. Knowledge of program behavior is obtained experimentally, with repeated runs of a slightly modified version of the application or the same code in different environments. In these circumstances, comparative performance analysis can provide meaningful insights into the subtle effects of system and code changes on parallel program behavior by highlighting the difference in performance results across executions. I have designed and implemented modules which extend the PPerfDB performance tool to allow access to existing performance data generated by several commonly used tracing tools. Access occurs from within the experiment management framework provided by PPerfDB for the identification of system parameters, the representation of multiple sets of execution data, and the formulation of data queries. Furthermore, I have designed and implemented an additional module that will generate new data using dynamic instrumentation under the control of PPerfDB. This was done to enable the creation of novel experiments for performance hypothesis testing and to ultimately automate the diagnostic and tuning process. As data from such diverse sources has very different representations, various techniques to allow comparisons are presented. I have generalized the definition of the Performance Difference operator, which automatically detects divergence in multiple data sets, and I have defined an Overlay operation to provide uniform access to both dynamically generated and tracefile based data. The use and application of these new operations along with an indication of some of the issues involved in the creation of a fully automatic comparative profilier is presented via several case studies performed on an IBM SP2 using different versions of an MPI application.

Type classes, first proposed during the design of the Haskell programming language, extend standard type systems to support overloaded functions. Since their introduction, type classes have been used to address a range of problems, from typing ordering and arithmetic operators to describing heterogeneous lists and limited subtyping. However, while type class programming is useful for a variety of practical problems, its wider use is limited by the inexpressiveness and hidden complexity of current mechanisms. We propose two improvements to existing class systems. First, we introduce several novel language features, instance chains and explicit failure, that increase the expressiveness of type classes while providing more direct expression of current idioms. To validate these features, we have built an implementation of these features, demonstrating their use in a practical setting and their integration with type reconstruction for a Hindley-Milner type system. Second, we define a set-based semantics for type classes that provides a sound basis for reasoning about type class systems, their implementations, and the meanings of programs that use them.

Generalized algebraic data types (GADTs) are a type system extension to algebraic data types that allows the type of an algebraic data value to vary with its shape. The GADT type system allows programmers to express detailed program properties as types (for example, that a function should return a list of the same length as its input), and a general-purpose type checker will automatically check those properties at compile time. Type inference for the GADT type system and the properties of the type system are both currently areas of active research. In this dissertation, I attack both problems simultaneously by exploiting the symbiosis between type system research and type inference research. Deficiencies of GADT type inference algorithms motivate research on specific aspects of the type system, and discoveries about the type system bring in new insights that lead to improved GADT type inference algorithms. The technical contributions of this dissertation are therefore twofold: in addition to new GADT type system properties (such as the prevalence of pointwise type information flow in GADT patterns, a generalized notion of existential types, and the effects of enforcing the GADT branch reachability requirement), I will also present a new GADT type inference algorithm that is significantly more powerful than existing algorithms. These contributions should help programmers use the GADT type system more effectively, and they should also enable language implementers to provide better support for the GADT type system.

Thesis (M.Eng.)--Memorial University of Newfoundland, 1999. / Bibliography: leaves 100-102.

HOLCF is an interactive theorem proving system that uses the mathematics of domain theory to reason about programs written in functional programming languages. This thesis introduces HOLCF '11, a thoroughly revised and extended version of HOLCF that advances the state of the art in program verification: HOLCF '11 can reason about many program definitions that are beyond the scope of other formal proof tools, while providing a high degree of proof automation. The soundness of the system is ensured by adhering to a definitional approach: New constants and types are defined in terms of previous concepts, without introducing new axioms. Major features of HOLCF '11 include two high-level definition packages: the Fixrec package for defining recursive functions, and the Domain package for defining recursive datatypes. Each of these uses the domain-theoretic concept of least fixed points to translate user-supplied recursive specifications into safe low-level definitions. Together, these tools make it easy for users to translate a wide variety of functional programs into the formalism of HOLCF. Theorems generated by the tools also make it easy for users to reason about their programs, with a very high level of confidence in the soundness of the results. As a case study, we present a fully mechanized verification of a model of concurrency based on powerdomains. The formalization depends on many features unique to HOLCF '11, and is the first verification of such a model in a formal proof tool.

Constructs for functional and logic programming can be smoothly integrated into an existing object-oriented language. We demonstrate this in the context of C++ (a statically-typed object-oriented language with effects and parametric polymorphism) via two libraries: FC++ and LC++. FC++ is a library for functional programming in C++; FC++ supports higher-order polymorphic functions, lazy lists, and a small lambda language; it also contains a large library of useful functions, datatypes, combinators, and monads. LC++ is a library for logic programming in C++; LC++ provides the same general functionality as Prolog, including the ability to return query results lazily (one at a time). Both libraries are embedded in C++ so that they share C++'s static type system, and the library interfaces provide straightforward ways for code from within one paradigm to ``call out' to another. Our work describes the techniques used to implement these libraries in C++ and shows that the resulting multiparadigm language has useful applications in real-world domains. We also describe how many of the implementation techniques can be generalized from C++ and applied to other programming languages to yield similar results.

Cette thèse traite de la conception et implémentationd’un langage de programmation pour les systèmes detraitement de flux en temps réel, comme l’encodagevidéo. Le modèle des réseaux de Kahn est bien adaptéà ce domaine et y est couramment utilisé. Dans cemodèle, un programme consiste en un ensemble deprocessus parallèles communicant à travers des filesmono-producteur, mono-consommateur. La force dumodèle réside en son déterminisme.Les langages synchrones fonctionnels comme Lustresont dédiés aux systèmes embarqués critiques. Un programmeLustre définit un réseau de Kahn synchronequi peut être exécuté avec des files bornées et sans blocage.Cette propriété est garantie par un système detypes dédié, le calcul d’horloge, qui établit une échellede temps globale à un programme. Cette échelle detemps globale est utilisée pour définir les horloges, sé-quences booléennes indiquant pour chaque file, et àchaque pas de temps, si un processus produit ou consommeune donnée. Cette information sert non seulementà assurer la synchronie mais également à générerdu logiciel ou matériel à état fini.Nous proposons et étudions les horloges entières, unegénéralisation des horloges booléennes autorisant desentiers naturels arbitrairement grands. Les horlogesentières décrivent la production ou consommation deplusieurs valeurs depuis une même file au cours d’uninstant. Nous les utilisons pour définir la constructiond’échelle de temps locale, qui peut masquer despas de temps cachés par un sous-programme au contexteenglobant.Ces principes sont intégrés à un calcul d’horloge pourun langage fonctionnel d’ordre supérieur. Nous étudionsses propriétés et prouvons en particulier que lesprogrammes bien typés ne bloquent pas. Nous compilonsles programmes typés vers des circuits numériquessynchrones en adaptant le schéma de générationde code dirigé par les horloges de Lustre. L’informationde typage contrôle certains compromis entre temps etespace dans les circuits générés. / This thesis addresses the design and implementationof a programming language for real-time streaming applications,such as video decoding. The model of Kahnprocess networks is a natural fit for this area and hasbeen used extensively. In this model, a program consistsin a set of parallel processes communicating via singlereader, single writer queues. The strength of the modellies in its determinism.Synchronous functional languages such as Lustre arededicated to critical embedded systems. A Lustre programdefines a synchronous Kahn process network, thatis, which can be executed using finite queues and withoutdeadlocks. This is enforced by a dedicated type system,the clock calculus, which establishes a global timescale throughout a program. The global time scale isused to define clocks: per-queue boolean sequences indicating,for each time step, whether a process producesor consumes a token in the queue. This information isused both for enforcing synchrony and for generatingfinite-state software or hardware.We propose and study integer clocks, a generalizationof boolean clocks featuring arbitrarily big natural numbers.Integer clocks model the production or consumptionof several values from the same queue in the courseof a time step. We then rely on integer clocks to definethe local time scale construction, which may hide timesteps performed by a sub-program from the surroundingcontext.These principles are integrated into a clock calculus fora higher-order functional language. We study its properties,proving among other results that well-typed programsdo not deadlock. We adjust the clock-directedcode generation scheme of Lustre to generate finite-statedigital synchronous circuits from typed programs. Thetyping information controls certain trade-offs betweentime and space in the generated circuits.

Functional logic languages provide a powerful programming paradigm combining the features of functional languages and logic languages. However, current implementations of functional logic languages are complex, slow, or both. This thesis presents a scheme, called the Basic Scheme, for compiling and executing functional logic languages based on non-deterministic graph rewriting. This thesis also describes the implementation and optimization of a prototype of the Basic Scheme. The prototype is simple and performs well compared to other current implementations.

Ce mémoire vise à recenser les avantages et les inconvénients de l'utilisation du langage de programmation fonctionnel dynamique Scheme pour le développement de jeux vidéo. Pour ce faire, la méthode utilisée est d'abord basée sur une approche plus théorique. En effet, une étude des besoins au niveau de la programmation exprimés par ce type de développement, ainsi qu'une description détaillant les fonctionnalités du langage Scheme pertinentes au développement de jeux vidéo sont données afin de bien mettre en contexte le sujet. Par la suite, une approche pratique est utilisée en effectuant le développement de deux jeux vidéo de complexités croissantes: Space Invaders et Lode Runner. Le développement de ces jeux vidéo a mené à l'extension du langage Scheme par plusieurs langages spécifiques au domaine et bibliothèques, dont notamment un système de programmation orienté objets et un système de coroutines. L'expérience acquise par le développement de ces jeux est finalement comparée à celle d'autres développeurs de jeux vidéo de l'industrie qui ont utilisé Scheme pour la création de titres commerciaux. En résumé, l'utilisation de ce langage a permis d'atteindre un haut niveau d'abstraction favorisant la modularité des jeux développés sans affecter les performances de ces derniers. / This master's thesis aims at pinpointing the pros and cons of using the dynamic functionnal language Scheme for developing video games. The method used is first based on a theoretical approach. Indeed, the specific requirements for video game programming and a detailed description of relevant Scheme features are presented. Then, a practical approach is taken by presenting two video games developed using the Scheme language: Space Invaders and Lode Runner. Their development resulted in the creation of various domain-specific languages and libraries, such as an objec- oriented system and a coroutine system. Each of these are presented separately in their respective chapter. Finally, the experience achieved in this process is compared to the experience acquired by some video game companies that also used Scheme for the developpement of their titles. The use of Scheme allowed us to perform various high-level abstractions that improved the modularity of the video games developed, without affecting their performance.