Computer Science Theses and Dissertations

Permanent URI for this collection

https://hdl.handle.net/1794/2040

This collection contains some of the theses and dissertations produced by students in the University of Oregon Computer Science Graduate Program. Paper copies of these and other dissertations and theses are available through the UO Libraries.

Browse

Browsing Computer Science Theses and Dissertations by Author "Ariola, Zena"

Now showing 1 - 6 of 6
  • Thumbnail Image
    ItemOpen Access
    Compiling a New Kind of Faster Curry
    (University of Oregon, 2022-02-18) Hairapetian, Shant; Ariola, Zena
    Traditionally, programming languages based on lambda calculus such asHaskell and ML do not support functions with a number of arguments (or arity) greater than one. In these languages, currying emulates the passing of multiple arguments by accepting one argument at a time and returning a closure that accepts the next. This approach is inefficient from a performance perspective. As such, Downen et al [A faster Curry with Extensional Types] proposed the addition of a primitive, extensional function type that accepts all of its arguments at once. Though this new function type enabled optimization for functions across known types, generic types could not enjoy this optimization. In their follow-up paper [Kinds are Calling Conventions] Downen et al proposed a new kind of system which allows for statically tracking arity information about generic types, thereby enabling faster currying and efficient compilation for these generic types. This paper will discuss the implementation of both of these changes in GHC (Glasgow Haskell Compiler).
  • Thumbnail Image
    ItemOpen Access
    Properties of Sequent-Calculus-Based Languages
    (University of Oregon, 2018-04-10) Johnson-Freyd, Philip; Ariola, Zena
    Programmers don't just have to write programs, they are have to reason about them. Programming languages aren't just tools for instructing computers what to do, they are tools for reasoning. And, it isn't just programmers who reason about programs: compilers and other tools reason similarly as they transform from one language into another one, or as they optimize an inefficient program into a better one. Languages, both surface languages and intermediate ones, need therefore to be both efficiently implementable and to support effective logical reasoning. However, these goals often seem to be in conflict. This dissertation studies programming language calculi inspired by the Curry-Howard correspondence, relating programming languages to proof systems. Our focus is on calculi corresponding logically to classical sequent calculus and connected computationally to abstract machines. We prove that these calculi have desirable properties to help bridge the gap between reasoning and implementation. Firstly, we explore a persistent conflict between extensionality and effects for lazy functional programs that manifests in a loss of confluence. Building on prior work, we develop a new rewriting theory for lazy functions and control which we first prove corresponds to the desired equational theory and then prove, by way of reductions into a smaller system, to be confluent. Next, we turn to the inconsistency between weak-head normalization and extensionality. Using ideas from our study of confluence, we develop a new operational semantics and series of abstract machines for head reduction which show us how to retain weak-head reduction's ease of implementation. After demonstrating the limitations of the above approach for call-by-value or types other than functions, we turn to typed calculi, showing how a type system can be used not only for mixing different kinds of data, but also different evaluation strategies in a single program. Building on variations of the reducibility candidates method such as biorthogonality and symmetric candidates, we present a uniform proof of strong normalization for our mixed-strategy system which works so long as all the strategies used satisfy criteria we isolate. This dissertation includes previously published co-authored material.
  • Thumbnail Image
    ItemOpen Access
    Reflections of Closures
    (University of Oregon, 2024-03-25) Sullivan, Zachary; Ariola, Zena
    The idea that programs are data forms the bedrock of functional programming languages, but it is also found in object-oriented languages and recent iterations of systems languages. Since passing and returning programs as data is incompatible with the architecture of modern machines, implementations of such a feature gives rise to closures, which package code with the environment that it needs to run. The first implementations of these objects are as part of the runtime system of an abstract machine. However, to be able to optimize these structures, compiler writers often choose instead to embed this structure in their code when compiling to lower-level languages in a transformation called closure conversion. While this transformation and closures more generally are well studied with respect to certain types of programming languages, how such a language interacts with different evaluation strategies still remains unstudied in a theoretical setting. Moreover, the current approaches to performing, optimizing, and proving correct this transformation lack the flexibility of other language features. This thesis develops these ideas by presenting closure conversions for missing evaluation strategies, specifying a new implementation approach that allows for the flexible implementation and optimization of closures, and formalizing them in an intermediate language that captures multiple notions of closures and evaluation strategies in one. Our approach follows from first principles meaning that our closures are a reflection of the environment-based abstract machines that birth them. We develop an approach to reasoning about closures that connects their equational properties with the abstract machines on which they run. Thereby, we can prove not only that closure conversion does not change the output of programs, but that closure conversion removes the need for the runtime system to capture closures.
  • Thumbnail Image
    ItemOpen Access
    Sequent Calculus: A Logic and a Language for Computation and Duality
    (University of Oregon, 2017-09-06) Downen, Paul; Ariola, Zena
    Truth and falsehood, questions and answers, construction and deconstruction; most things come in dual pairs. Duality is a mirror that reveals the new from the old via opposition. This idea appears pervasively in logic, where duality inverts "true" with "false" and "and" with "or." However, even though programming languages are closely connected to logics, this kind of strong duality is not so apparent in practice. Sum types (disjoint tagged unions) and product types (structures) are dual concepts, but in the realm of programming, natural biases obscure their duality. To better understand the role of duality in programming, we shift our perspective. Our approach is based on the Curry-Howard isomorphism which says that programs following a specification are the same as proofs for mathematical theorems. This thesis explores Gentzen's sequent calculus, a logic steeped in duality, as a model for computational duality. By applying the Curry-Howard isomorphism to the sequent calculus, we get a language that combines dual programming concepts as equal opposites: data types found in functional languages are dual to co-data types (interface-based objects) found in object-oriented languages, control flow is dual to information flow, induction is dual to co-induction. This gives a duality-based semantics for reasoning about programs via orthogonality: checking safety and correctness based on a comprehensive test suite. We use the language of the sequent calculus to apply ideas from logic to issues relevant to program compilation. The idea of logical polarity reveals a symmetric basis of primitive programming constructs that can faithfully represent all user-defined data and co-data types. We reflect the lessons learned back into a core language for functional languages, at the cost of symmetry, with the relationship between the sequent calculus and natural deduction. This relationship lets us derive a pure lambda calculus with user-defined data and co-data which we further extend by bringing out the implicit control-flow in functional programs. Explicit control-flow lets us share and name control the same way we share and name data, enabling a direct representation of join points, which are essential for tractable optimization and compilation.
  • Thumbnail Image
    ItemOpen Access
    The Design of Intermediate Languages in Optimizing Compilers
    (University of Oregon, 2018-10-31) Maurer, Luke; Ariola, Zena
    Every compiler passes code through several stages, each a sort of mini- compiler of its own. Thus each stage may deal with the code in a different representation, which may have little to do with the source or target language. We can describe these in-memory representations as languages in their own right, which we call intermediate languages. Each intermediate language is designed to accomodate the stage of compilation that handles it. Those toward the end of the compilation pipeline, for instance, tend to have features expressing low-level details of computation. A subtler case is that of the optimization stage, whose role is to transform the program so that it runs faster, uses less memory, and so forth. The optimizer faces tradeoffs: The language should provide enough information to guide optimization algorithms, but all of this information must be kept up to date as the program is transformed. Also, establishing invariants in the language can be helpful both in implementing algorithms and in debugging the implementation, but each invariant may complicate desirable transformations or rule them out altogether. Finally, a ivlanguage where the invariants are obviously correct may have a form too awkward or otherwise unsuited to the compiler’s needs. Given the properties and invariants that we would like the language to provide, we can approach the design task in a way that gives these features without necessarily sacrificing implementability. Namely, begin with a formal language that makes the desired properties obvious, then translate it to one more suitable for implementation. We can even translate theorems about valid transformations in the formal language to derive correct algorithms in the implementation language. This dissertation explores the connections between different intermediate languages and how they can be interderived, then demonstrates how translation lead to an improvement to the Glasgow Haskell Compiler opimization engine. This dissertation includes previously published coauthored material.
  • Thumbnail Image
    ItemOpen Access
    The Essence of Codata and Its Implementations
    (University of Oregon, 2018-09-06) Sullivan, Zachary; Ariola, Zena
    Data types are a widely-used feature of functional programming languages that allow programmers to create abstractions and control branching computations. Instances of data types are introduced by applying one of a disjoint set of constructors and are eliminated by pattern matching on the constructor used. Dually, codata types are defined by their destructors, are introduced by copattern matching on their context, and eliminated by applying destructors. We extend motivation for codata types to include adding types that satisfy the extensional laws and adding an abstraction for constraining clients of code. We also improve on work implementing codata by developing an untyped compilation technique for codata that works for both call-by-name and call-by-value evaluation strategies and scales to simple and indexed type systems. We demonstrate the practicality of our technique by implementing a prototype compiler and a Haskell language extension.