Supervised Student Activities

  • Yawar Raza
    A Mechanized Proof in Coq of the Type Soundness of Core L3
    (MS Project Course)

    S20175; MS Project Course Final Report

  • Anindo Saha, Bhavin Shah
    Functional Programming and Haskell
    (Independent Study)

    S20175;

  • Kyle Savarese
    Formal Verification of Voting Receipts in Chaums's Scheme
    (MS Thesis)

    In the aftermath of the United States Presidential election, more and more frequently there are calls for voters to be able to place their votes from the comfort of their own home. However, many studies have found prototype systems to be either insecure or insufficiently defined for the purposes of an election on a national scale.

    In this paper I will examine the security of voting applications from a different angle: the validation and verification of compiled code. There are the obvious concerns about unverified code, that we have no guarantee the protocol described by the voting procedure is the one being executed. Using work by Appel as a model, it can be seen that even advanced cryptographic algorithms can be verified. Using Chaum's scheme, a visual cryptography system intensely examined in Staub's work, and originally described in Chaum's paper, as our target enables us to have a secure algorithm that we can properly verify. Our goal will be to establish a verified code implementation for Chaum's scheme that could be deployed to voters to confirm their votes.

    S20165; MS Thesis

  • Srinath Kanna Dhandapani
    Implementation of Partial Redundancy Elimination (PRE) for MLton Compiler
    (MS Project Course)

    The goal of the project is to implement the GVN-PRE optimization pass in MLton, for eliminating partial redundancies. With the integration of this pass in MLton, all kinds of full redundancies should automatically be eliminated and also perform loop invariant code motion along with it. The same pass can be extended for eliminating redundancies with constructors and tuples having higher register loads along with eliminating simple expressions. This optimization can be used to perform various other improvements in the resulting code like eliminating code segments based on known cases.

    S20165; MS Project Course Final Report

  • Theodore Sill
    Type Annotation Analysis Using the .NET Compiler Platform
    (MS Project Course)

    Programming language type and runtime systems provide powerful guarantees about the behavior of a program when it is executed. However, they do not always ensure that a program will have the desired runtime characteristics, or that the outcomes will align with the intent of the programmer. It is often necessary to provide additional assurances that a program is correct in this sense. Type annotation analysis frameworks are static analysis tools that allow programmers to add additional information in the form of type annotations, and thus express their intent in such a way that it may be automatically verified.

    In the past, creating a type annotation analysis tool would have been a large undertaking. Most compilers were black boxes which accepted source files as input and produced an executable as output. Those wishing to make use of a program representation, such as an Abstract Syntax Tree (AST), were forced to construct their own. Microsoft opened this black box when they delivered the .NET Compiler Platform (code named "Roslyn"), which exposes several APIs.

    In this work, we will explore these offerings and describe how they were leveraged to build a type annotation analysis tool for C#. We call this tool "Sharp Checker" in homage to the Checker Framework, which is a full-featured solution for Java. The contribution of this work is to translate the mechanisms of annotation processing at work in tools like the Checker Framework to the Visual Studio IDE, where users receive feedback immediately as they type and upon compilation. Sharp Checker may be installed as a NuGet package, and the source code is available on GitHub. We have demonstrated Sharp Checker's extensibility and usefulness by implementing the Encrypted, Nullness, and Tainted annotated type systems and applying them to the Sharp Checker source code, as well as publicly available applications. In the process, we discovered and corrected several bugs, while gaining insights into the properties which may be enforced by type annotation analysis.

    S20165; MS Project Course Final Report

  • Matt Gambogi, Thomas Logan, John Renner, Ziwei Ye
    Mechanized Meta-Theory for Programming Languages
    (Independent Study)

    S20165;

  • Ross Bayer
    Compiler Construction II
    (Independent Study)

    S20161; Independent Study Report

  • Juraj Culak, Stephen Demos, Robert Glossop, Alexander Kyte, David Narvaez, Krishna Ravikumar, Yawar Raza, Kyle Savarese
    Mechanized Meta-Theory for Programming Languages
    (Independent Study)

    S20155;

  • Krishna Ravikumar
    Supporting Vector Expressions and Patterns in MLton
    (MS Project Course)

    Standard ML (SML) is a strict, statically-typed functional programming language. Two of the most popular compilers for SML are MLton and Standard ML of New Jersey (SML/NJ). In the SML language, vectors are homogeneous, immutable arrays. Vectors are a standard feature of SML'97, but SML/NJ also has special syntax for vector expressions and vector patterns. In MLton, as with SML'97, vectors can be created only through the Vector structure, and cannot be pattern-matched. The project aims to implement support for vector expressions and patterns similar to what SML/NJ offers, and introduce representation for such vectors internally so that optimizations on them are possible.

    S20155; MS Project Course Final Report

  • Matthew Surawski
    Loop Optimizations for MLton
    (MS Project Course)

    This report discusses the design and implementation of loop optimizations for the MLton Standard ML compiler. The loops that programmers typically write do not take advantage of the full capabilities of modern processors. Recognizing and transforming these loops into alternate forms that better match the capabilities of the hardware can result in significant performance gains without a significant increase in code size.

    The specific optimizations examined are loop unswitching and loop unrolling. Unswitching is a transformation that moves conditional branches on loop-invariant conditions outside the loop. Unrolling transforms a loop of known iteration count into a larger loop with a reduced iteration count, or eliminates the loop entirely and replaces it with straight-line code. These transformations are implemented as optimization passes on MLton's Static Single Assignment intermediate form. In order to measure the benefits of these optimizations, MLton's benchmark suite is run against the modified compiler. The resulting execution times and binary sizes show that these optimizations can introduce significant performance improvements without unacceptably increasing the size of the program.

    S20155; MS Project Course Final Report

  • Ryan Shea
    Alternate Control-Flow Analyses for Defunctionalization in the MLton Compiler
    (MS Project Course)

    In the compilation of a program, the compiler will translate the written code into a binary capable of being run by a computer. During this process it is common for there to be several intermediate representations of the code to make different parts of the compilation easier, quicker, or more efficient. One of the translations into an intermediate state for functional programming languages is known as closure conversion, which is handled by the defunctionalization pass in the MLton compiler. This process involves the conversion of the higher-order program representation into a first-order program representation through the use of closure applications at every function call site. In this process, Control-Flow analyses (CFAs) interpret the possible functions that can be applied at a now first-order location in the program so that a proper closure of functions that represent the higher-order equivalent at that location can be created. In this paper we look at the precision of a Simply-Typed analysis, 0-CFA, and m-CFA by comparing their overall member size distributions for each of these closure conversions. We use the MLton compiler for Standard ML as the framework within which to analyze these three CFAs.

    S20155; MS Project Course Final Report

  • Vedant Raiththa
    Source-Level Debugging for MLton
    (MS Project Course)

    This project explored developing a simple source-level debugger for MLton. MLton already supported source-level profiling, which can be used to attribute bytes allocated or time spent in source functions. This feature is used in conjunction with the LLVM code generator to emit LLVM debugging intrinsics. This yielded basic source-level debugging support, with the ability to set/unset breakpoints and step through declarations and functions.

    S20151; MS Project Course Final Report

  • Kevin Bradley
    Compiler Optimization Techniques
    (Independent Study)

    S20148; Independent Study Report

  • Michael Peterson
    Compiler Construction
    (Independent Study)

    S20148; Independent Study Report

  • Kevin Bradley
    Successor ML Features for MLton
    (MS Project Course)

    This project aims to extend the MLton implementation of Standard ML by adding in new language features. Over time the Standard ML programming community has identified various language features and extensions, known as Successor ML which should prove useful in practice. The goal of this project is to identify and implement a subset of these features in the MLton compiler. This report presents the selected features, their syntax, motivation, and the details behind their implementation. The selected features are comprised of line comments, do declarations, optional pattern bars, disjunctive patterns, record extension & update, record punning, extended literals, optional semicolons, and withtype for signatures.

    S20145; MS Project Course Final Report

  • Alexander Kyte
    Garbage Collection
    (Independent Study)

    S20141; Independent Study Report

  • Angel Cambero Ramos
    Object-oriented Programming, Functional Programming and Design Patterns using Scala, Ruby and Java
    (Independent Study)

    S20138; Independent Study Report

  • Alexander Dean
    Process Cooperativity as a Feedback Metric in Concurrent Message-Passing Languages
    (MS Thesis)

    Runtime systems for concurrent languages have begun to utilize feedback mechanisms to influence their scheduling behavior as the application proceeds. These feedback mechanisms rely on metrics by which to grade any alterations made to the schedule of the multi-threaded application. As the application's phase shifts, the feedback mechanism is tasked with modifying the scheduler to reduce its overhead and increase the application's efficiency.

    Cooperativity is a novel possible metric by which to grade a system. In biochemistry the term cooperativity is defined as the increase or decrease in the rate of interaction between a reactant and a protein as the reactant concentration increases. This definition translates well as an information theoretic definition as: the increase or decrease in the rate of interaction between a process and a communication method as the number of processes increase.

    This work proposes several feedback mechanisms and scheduling algorithms which take advantage of cooperative behavior. It further compares these algorithms to other common mechanisms via a custom extensible runtime system developed to support swappable scheduling mechanisms. A minimalistic language with interesting characteristics, which lend themselves to easier statistical metric accumulation and simulated application implementation, is also introduced.

    Defended: August 12, 2014; MS Thesis

  • Connor Adsit, Danilo Dominguez Perez, Matthew Le
    Mechanized Meta-Theory for Programming Languages
    (Independent Study)

    S20135; Independent Study Report (Adsit), Independent Study Report (Dominguez Perez), Independent Study Report (Le)

  • Jose Raymundo Cruz Henriquez
    HsOptions: Haskell Command-line Flags Processing Library
    (MS Project Course)

    S20135; MS Project Course Final Report

  • Jedd Haberstro
    Formal Verification of Compilers
    (Independent Study)

    S20131; Independent Study Report

  • Anthony Castiglia
    Efficient Closure Conversion in LangF
    (MS Project Course)

    S20131; MS Project Course Final Report

  • Prashanth Tilleti
    Correctly Rounded Floating-point Binary-to-Decimal and Decimal-to-Binary Conversion Routines in Standard ML
    (MS Project Course)

    S20131; MS Project Course Final Report

  • Russell Harmon
    Introspection via Self Debugging
    (MS Project)

    The omnipresent support for introspection in modern programming languages indicates the usefulness of the tool. Unfortunately, C, which is one of the most pervasive programming languages and the foundation of nearly every modern operating system, does not support introspection.

    By leveraging an existing debugger, an API entitled Ruminate brings introspection to the programming language C. Debuggers have long had access to the type information which is needed for introspection. On most UNIX platforms, this is accomplished by the debugger reading any debugging symbols which may be present in the target binary, and inspecting the state of the target program. These debugging symbols are not present by default and the compiler must be instructed to add the symbols at compile time. These techniques are leveraged to gain the information which is needed to create an introspection API and building on that, an API which can convert arbitrary types to and from JSON.

    Defended: December 12, 2013; MS Project

  • Edward Amsden
    TimeFlies: Push-Pull Signal-Function Functional Reactive Programming
    (MS Thesis)

    Functional Reactive Programming (FRP) is a promising class of abstractions for interactive programs. FRP systems provide values defined at all points in time (behaviors or signals) and values defined at countably many points in time (events) as abstractions.

    Signal-function FRP is a subclass of FRP which does not provide direct access to time-varying values to the programmer, but instead provides signal functions, which are reactive transformers of signals and events, as first-class objects in the program.

    All signal-function implementations of FRP to date have utilized demand-driven or "pull-based" evaluation for both events and signals, producing output from the FRP system whenever the consumer of the output is ready. This greatly simplifies the implementation of signal-function FRP systems, but leads to inefficient and wasteful evaluation of the FRP system when this strategy is employed to evaluate events, because the components of the signal function which process events must be computed whether or not there is an event occurrence.

    In contrast, an input-driven or "push-based" system evaluates the network whenever new input is available. This frees the system from evaluating the network when nothing has changed, and then only the components necessary to react to the input are re-evaluated. This form of evaluation has been applied to events in standard FRP systems but not in signal-function FRP systems.

    I describe the design and implementation of a signal-function FRP system which applies pull-based evaluation to signals and push-based evaluation to events (a "push-pull" system). The semantics of the system are discussed, and its performance and expressiveness for practical examples of interactive programs are compared to existing signal-function FRP systems through the implementation of a networking application.

    Defended: August 19, 2013; MS Thesis

  • Brian Leibig
    An LLVM Backend for MLton
    (MS Project)

    This report presents the design and implementation of a new LLVM back-end for the MLton Standard ML compiler. The motivation of this project is to utilize the features that an LLVM back-end can provide to a compiler, and compare its implementation to the existing back-ends that MLton has for C and native assembly (x86 and amd64). The LLVM back-end was found to offer a greatly simpler implementation compared to the existing back-ends, along with comparable compile times and performance of generated executables, with the LLVM-compiled version performing the best on many of the benchmarks.

    Defended: August 8, 2013; MS Project

  • Alexander Dean
    Runtime Scheduling in Functional Languages
    (Independent Study)

    Q20124; Independent Study Report

  • Daniel Rosenwasser
    Topics in Closure Conversion
    (Independent Study)

    Q20123; Independent Study Report

  • Brian Leibig
    Compiler Optimizations with LLVM
    (Independent Study)

    Q20121; Independent Study Report

  • Alexander Dean
    Memory Models and Determinism for Concurrent/Parallel Programming Languages
    (Independent Study)

    Q20113; Independent Study Report

  • Kyle Theriault
    Software Testing
    (Independent Study)

    Q20104; Independent Study Report

  • Ben Holm
    Evaluation of RSL History as a Tool for Assistance in the Development and Evaluation of Computer Vision Algorithms
    (MS Thesis; co-advised)

    A revision of Recognition Strategy Language (RSL), a domain-specific language for pattern recognition algorithm development, is in development. This language provides several tools for pattern recognition algorithm implementation and analysis, including composition of operations and a detailed history of those operations and their results. This research focuses on that history and shows that for some problems it provides an improvement over traditional methods of gathering information.

    When designing a pattern recognition algorithm, bookkeeping code in the form of copious logging and tracing code must be written and analyzed in order to test the effectiveness of procedures and parameters. The amount of data grows when dealing with video streams; new organization and searching tools need to be designed in order to manage the large volume of data. General purpose languages have techniques like Aspect Oriented Programming intended to address this prob- lem, but a general approach is limited because it does not provide tools that are useful to only one problem domain. By incorporating support for this bookkeeping work directly into the language, RSL provides an improvement over the general approach in both development time and ability to evaluate the algorithm being designed for some problems.

    The utility of RSL is tested by evaluating the implementation process of a computer vision algorithm for recognizing American Sign Language (ASL). RSL history is examined in terms of its use in the development and evaluation stages of the algorithm, and the usefulness of the history is stated based on the benefit seen at each stage. RSL is found to be valuable for a portion of the algorithm involving distinct steps that provide opportunity for comparison. RSL was less beneficial for the dynamic programming portion of the algorithm. Compromises were made for performance reasons while implementing the dynamic programming solution and the inspection at every step of what amounts to a brute-force search was less informative. We suggest that this investigation could be continued by testing with a larger data set and by comparing this ASL recognition algorithm with another.

    Defended: August 8, 2011; MS Thesis

  • Justin Cady
    Functional Programming Applied to Web Development Templates
    (MS Project)

    In most web applications, the model-view-controller (MVC) design pattern is used to separate concerns of a system. However, the view layer, also referred to as the template layer, can often become tightly coupled to the controller. This lack of separation makes templates less flexible and reusable, and puts more responsibility in the controller's hands than what is ideal. A better solution is to give the template layer more control over the data it presents and limit the controller's influence on presentation. The jtc template engine uses elements of functional programming to empower templates by treating templates as functions.

    Defended: May 31, 2011; MS Project

  • Edward Amsden
    Functional Reactive Programming
    (Independent Study)

    Q20103; Independent Study Report

  • Justin Cady
    Functional Programming & Web Frameworks
    (Independent Study)

    Q20102; Independent Study Report

  • Karl Voelker
    Practical Programming with Total Functions
    (MS Thesis)

    Functional programming offers an advantage over imperative programming: functional programs are easier to reason about and understand, which makes certain classes of errors less common. Yet, the two disciplines have some pitfalls in common: any computation, functional or not, may be non-terminating, or may terminate in a run-time error. Turner describes a discipline called "Total Functional Programming" (TFP) in which these pitfalls are impossible, due to some easily-checked rules which require all recursion to be done structurally.

    In this report, I detail my findings about the practical benefits and limitations of total functional programming, as well as the interactions which arise between TFP and the design and implementation of a rich functional programming language. These findings are the result of implementing a TFP compiler as a modification of the Glasgow Haskell Compiler (GHC), as well as a total standard library and a variety of total example programs.

    Defended: July 27, 2010; MS Thesis