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.

Dependent type theory is a proven technology for verified functional programming in which programs and their correctness proofs may be developed using the same rules in a single formal system. In practice, large portions of programs developed in this way have no computational relevance to the ultimate result of the program and should therefore be removed prior to program execution. In previous work on identifying and removing irrelevant portions of programs, computational irrelevance is usually treated as an intrinsic property of program expressions. We find that such an approach forces programmers to maintain two copies of commonly used datatypes: a computationally relevant one and a computationally irrelevant one. We instead develop an extrinsic notion of computational irrelevance and find that it yields several benefits including (1) avoidance of the above mentioned code duplication problem; (2) an identification of computational irrelevance with a highly general form of parametric polymorphism; and (3) an elective (i.e., user-directed) notion of proof irrelevance. We also develop a program analysis for identifying irrelevant expressions and show how previously studied types embodying computational irrelevance (including subset types and squash types) are expressible in the extension of type theory developed herein.

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.

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.

Bootstrap is a computer-programming curriculum that teaches students to program video games using Racket, a functional programming language based on algebraic syntax. This study investigated the relationship between learning to program video games from a Bootstrap course and the resulting effect on students' understanding of algebra. Courses in three different schools, lasting about six weeks each, were studied. Control and treatment groups were given a pre and post algebra assessment. A qualitative component consisting of observations and interviews was also used to further triangulate findings. Statistical analysis revealed that students who completed the Bootstrap course gained a significantly better understanding of variables and a suggestive improvement in understanding functions. In the assessments, students failed to demonstrate a transfer of the advanced concepts of function composition and piecewise functions from programming to algebraic notation. Interviews with students demonstrated that with coaching, students were able to relate functions written in Racket to functions written in algebraic notation, but were not yet able to transfer their experience of function composition from programming to algebra.

The ideals of exact modeling, and of putting off approximations as long as possible, make Bayesian practice both successful and difficult. Languages for modeling probabilistic processes, whose implementations answer questions about them under asserted conditions, promise to ease much of the difficulty. Unfortunately, very few of these languages have mathematical specifications. This makes them difficult to trust: there is no way to distinguish between an implementation error and a feature, and there is no standard by which to prove optimizations correct. Further, because the languages are based on the incomplete theories of probability typically used in Bayesian practice, they place seemingly artificial restrictions on legal programs and questions, such as disallowing unbounded recursion and allowing only simple equality conditions. We prove it is possible to make trustworthy probabilistic languages for Bayesian practice by using functional programming theory to define them mathematically and prove them correct. The specifications interpret programs using measure-theoretic probability, which is a complete enough theory of probability that we do not need to restrict programs or conditions. We demonstrate that these trustworthy languages are useful by implementing them, and using them to model and answer questions about typical probabilistic processes. We also model and answer questions about processes that are either difficult or impossible to reason about precisely using typical Bayesian mathematical tools.

Functional and reactive programming patterns provide powerful sets of tools for dealing with complexity and scalability. These stand in stark contrast to the imperative programming patterns which permeate the industry. This report seeks to investigate the extent to which a set of common imperative programming languages can be used to implement such functional and reactive patterns, and what the implications of doing so are. This is done by implementing and using a framework based on such patterns in Java, Kotlin, Objective-C, and Swift. The results show that this is possible in all of these languages, but the extent to which this can be considered idiomatic is questionable. Upholding immutability and referential transparency is highlighted as the main source of concern in this regard. / Funktionella och reaktiva programmeringsmönster förser utvecklare med kraftfulla abstraktioner för att hantera komplexitet och skalbarhet. Dagens industri förlitar sig dock till en majoritet på imperativa programspråk, där dessa mönster inte nödvändigtvis kan utnyttjas. Syftet med denna rapport är därför att undersöka hur sådana mönster kan tillämpas i imperativa programspråk. Detta görs genom att studera implementationen och användandet av ett ramverk för funktionell och reaktiv programmering i fyra programspråk: Java, Kotlin, Objective-C och Swift. Rapporten finner att de mönster undersökta i denna rapport går att implementera med existerande språkfunktioner för alla dessa språk, men frågan om detta kan anses idiomatiskt är oklar. Det huvudsakliga problemet är att säkerställa att funktioner skrivs utan sidoeffekter och att datastrukturerna som används inte är muterbara.

Because of its security, high availability, and automatic memory management, the JVM (Java Virtual Machine) is a desirable execution environment. However, since the JVM was originally made for Java, which is an objectoriented language, it is hard for languages with other paradigms to run on it. This thesis explores the challenges of compiling a functional language for the JVM. We implement a backend generating JVM bytecode as an extension to the compiler of MCore, a minimal functional language based on the lambda calculus. The backend features two different ways of compiling functions. One generates classes representing functions and their environment at compile-time, and one creates these function classes dynamically at runtime. The two different versions of compiling functions are compared in regards to execution speed of the outputted bytecode, compiler output size, and recursion depth. The results show that the two different ways of compiling functions perform well on different metrics. / På grund av sin säkerhet, tillgänglighet och automatiska minneshantering är JVM:en (Java Virtual Machine) en önksvärd exekveringsmiljö. På grund av att JVM:en ursprungligen skapades för programmeringsspråket Java, som är ett objektorienterat språk, så är det svårt för språk som följer andra paradigmer att köra på JVM:en. Denna uppsats undersöker utmaningarna som uppstår vid kompilering av ett funktionellt språk på JVM:en genom en litteraturstudie. Vi implementerar en backend som genererar JVM bytekod som en utökning av kompilatorn för MCore, ett minimalt funktionellt språk baserat på lambdakalkylen. Backenden implementeras med två tekniker för att kompilera funktioner. Den ena genererar klasser som representerar funktioner och deras miljö under kompileringstiden och den andra genererar dessa funktionsklasser dynamiskt vid körtid. Vi jämför de två teknikerna med avseende på den producerade bytekodens exekveringstid, storlek och rekursionsdjup. Resultaten visar att de två kompilationsteknikerna av funktioner presterar olika på olika mätningar.

System-on-Chip (SoC) and other complex distributed hardware/software systems contain heterogeneous components whose behavior are best captured by different models of computations (MoCs). As a result, any system design framework for such systems requires the capability to express heterogeneous MoCs. Although a number of system level design languages (SLDL)s and frameworks have proliferated over the last few years, most of them are lacking in multiple ways. Some of the SLDLs and system design frameworks we have worked with are SpecC, Ptolemy II, SystemC-H, etc. From our analysis of these, we identify their following shortcomings: First, their dependence on specific programming language artifacts (Java or C/C++) make them less amenable to formal analysis. Second, the refinement strategies proposed in the design flows based on these languages lack formal semantics underpinnings making it difficult to prove that refinements preserve correctness, and third, none of the available SLDLs are easily customizable by users. In our work, we address these problems as follows: To alleviate the first problem, we follow Axel Jantsch's paradigm of function-based semantic definitions of MoCs and formulate a functional programming framework called SML-Sys. We illustrate through a number of examples how to model heterogenous computing systems using SML-Sys. Our framework provides for formal reasoning due to its formal semantic underpinning inherited from SML's precise denotational semantics. To handle the second problem and apply refinement strategies at a higher-level, we propose a refinement methodology and provide a semantics preserving transformation library within our framework. To address the third shortcoming, we have developed EWD, which allows users to customize MoC-specific visual modeling syntax defined as a metamodel. EWD is developed using a metamodeling framework GME (Generic Modeling Environment). It allows for automatic design-time syntactic and semantic checks on the models for conformance to their metamodel. Modeling in EWD facilitates saving the model in an XML-based interoperability language (IML) we defined for this purpose. The IML format is in turn automatically translated into Standard ML, or Haskell models. These may then be executed and analyzed either by our existing model analysis tools SMLSys, or the ForSyDe environment. We also generate SMV-based template from the XML representation to obtain verification models. / Master of Science

In functional programming it is common practice to build modular programs by composing functions where the intermediate values are data structures such as lists or arrays. A desirable optimisation for programs written in this style is to fuse the composed functions and thereby eliminate the intermediate data structures and their associated runtime costs. Stream fusion is one such fusion optimisation that can eliminate intermediate data structures, including lists, arrays and other abstract data types that can be viewed as coinductive sequences. The fusion transformation can be applied fully automatically by a general purpose optimising compiler. The stream fusion technique itself has been presented previously and many practical implementations exist. The primary contributions of this thesis address the issues of correctness and optimisation: whether the transformation is correct and whether the transformation is an optimisation. Proofs of shortcut fusion laws have typically relied on parametricity by making use of free theorems. Unfortunately, most functional programming languages have semantics for which classical free theorems do not hold unconditionally; additional side conditions are required. In this thesis we take an approach based not on parametricity but on data abstraction. Using this approach we prove the correctness of stream fusion for lists -- encompassing the fusion system as a whole, not merely the central fusion law. We generalise this proof to give a framework for proving the correctness of stream fusion for any abstract data type that can be viewed as a coinductive sequence and give as an instance of the framework, a simple model of arrays. The framework requires that each fusible function satisfies a simple data abstraction property. We give proofs of this property for several standard list functions. Previous empirical work has demonstrated that stream fusion can be an optimisation in many cases. In this thesis we take a more universal view and consider the issue of optimisation independently of any particular implementation or compiler. We make a semi-formal argument that, subject to certain syntactic conditions on fusible functions, stream fusion on lists is strictly an improvement, as measured by the number of allocations of data constructors. This detailed analysis of how stream fusion works may be of use in writing fusible functions or in developing new implementations of stream fusion.