This page is no longer maintained!
My current web page is here: https://eric.walkingshaw.net
Student Mentoring and Advising
Groups
Functional Programming Club
I was the faculty advisor for the OSU Functional Programming Club. This was a student-run, official OSU club for students (graduate and undergraduate) who are interested in functional programming. The club met weekly to learn, discuss, and explore functional programming together.
Lambda Reading Group
I was the founder and co-advisor (with Martin Erwig) of an informal group of students and faculty that met weekly to discuss a different research paper on programming languages. Most of the participants were programming languages graduate students, but we were also regularly joined by students from the theory and software engineering groups, by advanced undergraduate students, and even occasionally by local high school students.
Graduated Students
As a professor at Oregon State University, I was the major advisor for the following students. Working with these students was the highlight of my academic career, and I'm super proud of the work we did together. You can find their theses and project reports below.
Graduate students
- Parisa Ataei, PhD 2021
- Jeff Young, PhD 2021
- Fariba Khan, MS 2021
- Ghadeer Alkubaish, MS 2020
- Qiaoran Li, MS 2019
- Alex Grasley, MS 2018
- Mike McGirr, MS 2018
- Keeley Abbott, MS 2017
- Meng Meng, MS 2017
- Shujin Wu, MS 2017
- Spencer Hubbard, MS 2016
Undergraduate students
- Spencer Mitchell, RELU 2018–2019
- Miles Van de Wetering, Honors BS 2017
Student Theses and Project Reports
- Theory and Implementation of a Variational Database Management System[Abstract, PDF]PhD dissertation, Oregon State University, 2021
In this thesis, I present the variational database management system, a formal framework and its implementation for representing variation in relational databases and managing variational information needs. A variational database is intended to support any kind of variation in a database. Specific kinds of variation in databases have already been studied and are well-supported, for example, schema evolution systems address the variation of a database’s schema over time and data integration systems address variation caused by accessing data from multiple data sources simultaneously. However, many other kinds of variation in databases arise in practice, and different kinds of variation often interact, but these scenarios are not well-supported by the existing work. For example, neither the schema evolution systems nor the database integration systems can address variation that arises when data sources combined in one database evolve over time.
This thesis collects a large amount of work: It defines the variational database framework and the syntax and denotational semantics of the variational relational algebra, a query language for variational databases. It presents two use cases of the variational database framework that are based on existing datasets and scenarios that are partially supported by existing techniques. It presents the variational database management system which is a prototype of variational databases and variational relational algebra as an abstract layer written in Haskell on top of a traditional RDBMS. It also presents several theoretical results related to the framework and the query language, such as syntax-based equivalence rules that preserve the semantics of a query, a type system for ensuring that a variational query is well-formed with respect to the underlying variational schema, and a confluence property of the variational relational algebra type system with respect to the relational algebra type system and its denotational semantics.
- Variational Satisfiability Solving[Abstract, PDF]PhD dissertation, Oregon State University, 2021
Over the last two decades, satisfiability and satisfiability-modulo theory (SAT/SMT) solvers have grown powerful enough to be general purpose reasoning engines throughout software engineering and computer science. However, most practical use cases of SAT/SMT solvers require not just solving a single SAT/SMT problem, but solving sets of related SAT/SMT problems. This discrepancy was directly addressed by the SAT/SMT community with the invention of incremental SAT/SMT solving. However, incremental SAT/SMT solvers require users to hand write a program which dictates the terms that are shared between problems and terms which are unique. By placing the onus on users, incremental solvers couple the users’ solution to the users’ exact sequence of SAT/SMT problems–making the solution overly specific–and require the user to write extra infrastructure to coordinate or handle the results.
This dissertation argues that the aforementioned problems result from accidental complexity produced by solving a problem that is variational without the concept of variation, similar to problematic use of GOTO statements in the absence of WHILE loop constructs. To demonstrate the argument, this thesis applies theory from variational programming to the domain of SAT/SMT solvers to create the first variational SAT solver. To do so, the thesis formalizes a variational propositional logic and specifies variational SAT solving as a compiler that compiles variational SAT problems to instructions for an industrial strength SAT solver.
- Formal Verification of the Variational Database Management System[Abstract, PDF]MS thesis, Oregon State University, 2021
Variation in data is abundant and ubiquitous in real-world applications. Managing variation in databases is, however, difficult and has been extensively studied by the database community. Schema evolution, data integration, and database versioning are examples of well-studied forms of database variation with effective context-specific solutions. However, variation appears in different forms and contexts in databases, and existing approaches cannot be generalized to handle arbitrary forms of variation irrespective of the context. Moreover, in practice, different forms of variation intersect in a particular context. Variational databases (VDB) provide a fundamental solution to variation management by explicitly encoding variation into relational databases that allows addressing different kinds of variation simultaneously. To support expressing variation in information need, traditional relational algebra (RA) is extended to variational relational algebra (VRA). VRA comes with a static type system that checks the validity of variational queries written in VRA. This thesis extends the formalization and formally verifies properties of the variational database management system (VDBMS). Variational sets and set operations definitions are formally verified and VDBs are formally encoded using them. Then, the correctness of the VRA type system with respect to the RA type system is formally specified and verified. VDBMS also allows writing variational queries without repeating variations that are already encoded in the VDB and sub-queries. These implicitly annotated v-queries get explicitly annotated by the system. Therefore, this thesis further formally verifies the process of explicitly annotating variational queries.
- Integrating Side Effects in Variational Programs Using Algebraic Effects[Abstract, PDF]MS thesis, Oregon State University, 2020
Variational programming supports efficiently executing many related programs at once by encoding all of the programs in one “variational program” that captures the differences among them statically and explicitly. An open problem in variational programming is how to handle side effects–if two program variants perform different side effects, we cannot separate the effect of one variant from the other since the outside world is not variational. A potential solution is to create variation-aware execution environments for variational programs, for example, a variational file system that keeps track of file variants corresponding to program variants. However, it is infeasible to do this for all kinds of effects. Also, there are different ways to handle the interaction of effects and variation that are incompatible with each other, preventing a one-size-fits-all solution. In this thesis, we argue that algebraic effects can be used to resolve the problem of combining variation and effects by enabling programmers to flexibly and incrementally extend a variational programming environment to handle new kinds of effects. We present a proof-of-concept prototype in the Eff programming language that demonstrates how a variational programming environment can be extended to support file input/output. Crucially, such extensions are done at the library level, which enables handling new kinds of effects and handling existing effects in multiple ways, both of which are essential in variational programming applications.
- Application of the Variational Database Management System to Schema Evolution and Software Product Lines[Abstract, PDF]MS project, Oregon State University, 2019
As a general solution to the problem of managing structural and content variability in relational databases, in previous work we have introduced the Variational Database Management System (VDBMS). VDBMS consists of a representation of a variational database (VDB) and a corresponding typed query language (v-query). However, since this is a novel database representation, there are no existing instances of VDBs or v-queries that can be used to evaluate the VDBMS. In this project, we present two case studies to demonstrate the use of VDBMS and support its evaluation. The case studies were constructed by systematically encoding variability scenarios from prior work and generating corresponding VDBs by adapting existing widely-used data sets. The first case study shows how to use the VDBMS to manage database variants under a schema evolution scenario. The second case study demonstrates how to integrate the VDBMS with a database-backed software product line. Each case study provides a VDB and a set of v-queries that will be used to evaluate the VDBMS. Additionally, we provide some insights into generating VDBs from relational databases that could assist future VDBMS users.
- Imperative Programming with Variational Effects[Abstract, PDF]MS thesis, Oregon State University, 2018
Variation is a commonly encountered element of modern software systems. Recent research into variation has led to increasing interest in the development of variational programming languages and corresponding variational models of execution. Variational imperative languages pose a particular challenge due to the complex interactions between side effects and variation. The development of interpreters for variational imperative languages has produced a number of techniques to address these interactions. This thesis builds upon and formalizes these techniques by defining a formal operational semantics for a simple imperative language that supports both variation and common side effects. We also provide an example of the successful implementation of these techniques in the form of the Resource DSL. One area in which variation is frequently encountered is in defining configurations and resource requirements for the deployment of modern software systems. To this end, we have developed the Resource DSL, a language that aids in the specification of resource requirements for highly configurable software systems.
- The Ownership Monad[Abstract, PDF]MS project, Oregon State University, 2018
The Rust programming language is a systems programming language with a strong static type system. A central feature of Rust’s type system is its unique concept of “ownership”, which enables Rust to give a user safe, low-level control over resources without the overhead of garbage collection. In Haskell, most data is immutable and many of the problems addressed by ownership in Rust simply don’t arise. However, ownership is still useful in Haskell in the context of mutable references and concurrency. This project report introduces the Ownership Monad, a monad that implements aspects of Rust’s ownership system as a library in Haskell. This will demonstrate many of the rules enforced by the ownership system in Rust in order to better understand the ownership-based method of tracking resources. This report will further explore the benefits such a system can provide for tracking resource use between concurrent threads.
- Formative Work Toward a Mixed-Initiative Programming Language[Abstract, PDF]MS thesis, Oregon State University, 2017
Mixed-initiative programming entails collaboration between a computer system, and a human to achieve some desired goal or set of goals. Often these goals change or are amended in real time during the course of program execution. As such, the plans these programs are based on must adapt and evolve to accommodate this iterative process. This thesis collects a literature review of research done in the field of mixed-initiative programs that provides an understanding of the problems faced when attempting to integrate computer systems and human users, a previously published paper with formative work in understanding how humans write programs for other humans, and finally some initial work done to develop an embedded domain-specific language for mixed-initiative drone control.
- Principles of Variational Databases[Abstract, PDF]MS thesis, Oregon State University, 2017
Data variations are prevalent in real-world applications. For example, software vendors have to handle numerous variations in the business requirements, conventions, and environmental settings of a software product. In database-backed software, the database of each version may have a different schema and content. As another example, data scientists often need to use a subset of the available databases because using non-relevant information may reduce the effectiveness of the results. Such variations give rise to numerous data variants in these applications. Users often would like to query and/or analyze all such variants simultaneously. For example, a software vendor would like to perform common tests over all versions of its product and a data scientist would like to find the subset of information over which the analytics algorithm delivers the most accurate results. Currently, there is not any systematic and principled approach to managing and querying data variations and users have to use their intuition to perform such analyses. We propose a novel abstraction called a variational database that provides a compact and structured representation of general forms of data variations for relational databases. As opposed to data integration approaches that provide a unified representation of all data sources, variational databases make variations explicit in both the schema definition and the query language without introducing too much complexity.
- Implementation Techniques for Variational Data Structures[Abstract, PDF]MS thesis, Oregon State University, 2017
Many applications require not only representing variability in software and data, but also computing with it. To do so efficiently requires variational data structures that make variability explicit in the underlying data and the operations used to manipulate it. Variational data structures have been developed ad hoc for many applications, but there is little general understanding of how to design them or what tradeoffs exist among them.
In this thesis, we introduce the concept of holes to represent variational data structures of different sizes and shapes. Moreover, we strive for a more systematic exploration and analysis of a variational data structure. We want to know how different design decisions affect the performance and scalability of a variational data structure, and what properties of the underlying data and operation sequences need to be considered.
Specifically, we study several alternative designs of a variational stack and analyze how these design decisions affect the performance of a variational stack with different usage profiles. We evaluate variational stacks in a real-world scenario: in the interpreter VarexJ when executing real software containing variability. Finally, we discuss different ways of representing variational priority queues and show how this affects the performance of the variational Dijkstra’s algorithm.
- View-Based Editing of Variational Code[Abstract, PDF]Honors BS thesis, Oregon State University, 2017
This paper discusses the merits of providing users variational views when editing variational code. I provide a plugin for the popular Atom Integrated Development Environment (IDE) which replaces #ifdef annotations commonly used by the C PreProcessor (CPP) with colored backgrounds, thus reducing code clutter and attempting to help programmers quickly distinguish code that belongs to different features. I also provide a number of helpful features designed to help the programmer create, remove, and refactor feature code. Finally, I present a user study conducted in order to determine how helpful each of the two main features (code folding and background color) are to programmers – it was determined that while there were no significant differences in efficiency or accuracy, the user experience was considerably enhanced.
- A Template CoprHD Storage Driver Based on the Southbound SDK[Abstract, PDF]MS project, Oregon State University, 2017
CoprHD is an open source software-defined storage and API platform which creates an abstraction layer over multi-vendor heterogeneous storage systems. It offers the ability to discover, pool and automate the management of the storage ecosystem with the help of storage drivers establishing connections between CoprHD and storage systems. On the demand of attracting more attentions from third-party storage companies, CoprHD community proposed a southbound driver SDK to simplify the process of developing a storage driver for CoprHD. ScaleIO storage driver, being the first one based on this southbound SDK, is implemented by us with Intel and EMC to serve the purposes to verify the southbound SDK and explore an effective way for the third-party driver development. This ScaleIO storage driver also acts as a template driver for the CoprHD community.
- A Formal Foundation for Variational Programming Using the Choice Calculus[, PDF]MS thesis, Oregon State University, 2016