lkuper@cs.indiana.edu
"We are using here a powerful strategy of synthesis: wishful thinking."
— Structure and Interpretation of Computer Programs, section 2.1.1
I'm a Ph.D. student in the School of Informatics and Computing at Indiana University, where I'm a member of the Programming Languages Group. Before starting at IU in 2008, I spent some years working in industry; before that, I got my BA in Computer Science and Music from Grinnell College in 2004. (CV: pdf, txt)
Kahn process networks, Haskell's monad-par library, and Intel's Concurrent Collections language are three diverse examples of deterministic-by-construction models of parallel computation, which offer programmers the promise of freedom from subtle, hard-to-reproduce nondeterministic bugs like race conditions. The determinism of all of these models hinges on a notion of monotonic data structures—data structures in which mutators may only add information, never destroy it. With monotonic data structures as a guiding principle, Ryan Newton, Amr Sabry, and I are working on developing a deterministic parallel programming model that is general enough to express existing models as well as guide the design of new ones. We're just getting started with this project; more details to come soon!
Languages with parametric polymorphism provide the compile-time guarantee that programs behave uniformly regardless of the types they are instantiated with. In such languages, this parametricity guarantee forms the basis of data abstraction and makes possible Wadler's "theorems for free!" In my current project with Amal Ahmed and Jacob Matthews (that expands on the work presented in their ESOP 2008 paper of the same title), I'm proving parametricity for a multi-language system that combines System F with a Scheme-like language by the use of dynamic sealing, which enforces data abstraction by using uniquely generated keys to seal values that should be kept opaque. While the use of sealing for this purpose has been suggested before, it has not previously been shown to preserve parametricity. Our proof employs a cross-language, step-indexed logical relation that uses possible worlds to model the semantics of key generation. Using this possible-worlds semantic model, we can show two results: first, that System F's parametricity guarantee is preserved when interoperating with Scheme, and, second, that parametricity is preserved in a Scheme-only setting that interacts with System F only to implement a polymorphic contract system.
I gave a talk about this project at the Northeastern University Programming Languages Seminar in February 2011. [slides]
Early designs for the Rust programming language featured a lightweight, structural, prototype-based object system—an unusual choice, since almost all prototype-based object systems are found in dynamically typed languages such as Self and JavaScript. Implementing such a system poses an interesting challenge for a language like Rust that statically guarantees type safety, since dynamic object extension and method overriding cause the type of the current object to change at run-time. While working on the Rust team at Mozilla in 2011, I implemented self-dispatch, object extension, and method overriding in the then-current Rust object system and learned that those features interact with each other in interesting ways. I gave a talk about the work I did on Rust to my research group in September 2011. [slides]
Junghee Lim and Thomas Reps' Transformer Specification Language (TSL) system comprises a domain-specific programming language for specifying the semantics of a processor at the level of the instruction set architecture, together with a run-time system for generating static analysis engines for executables compiled for that instruction set. TSL's ability to generate static analysis engines from ISA specifications makes it a powerful tool for analyzing executables, but it's of limited value if the ISA specifications are wrong in the first place. We are therefore interested in verifying the correctness of TSL's ISA specifications.
Working in collaboration with David Melski and the research team at GrammaTech, I implemented a system for testing TSL specifications. Given a CPU emulator generated from a TSL spec, our system attaches the emulator to a Linux process running on a physical CPU, initializes the emulator's state from that of the process, and compares the states of the emulated and physical CPUs after the execution of each instruction. If the states differ, the specification from which the emulator was generated was probably wrong. Our emulator testing framework is flexible enough that it could be extended to support testing of abstract emulators that have an abstract interpreter at their core, in addition to the concrete CPU emulators it supports now.
This work was done as part of the Safety in Numbers project and appears in the Safety in Numbers technical report (November 2010). I also gave a talk about the project in October 2010. [slides]
miniKanren is a declarative logic programming system implemented in
a pure functional subset of Scheme. In 2009, I worked
with Dan Friedman
and
collaborators
on implementing a pattern matcher for miniKanren. Our self-imposed
challenge was to implement the pattern matcher using
Scheme's syntax-rules macro system, as opposed to a
more powerful macro system such as syntax-case. Our
pattern matcher implementation uses CPS macros to control
the order in which macro expansion takes place, delaying expansion
of a macro that generates variable bindings until after other macro
expansions have happened. The ability to control the order in which
our macros expand allows us to generate more concise code. However,
we discovered a situation in which delayed expansion caused
incorrect code to be generated, leaving variables unbound that
should have been bound. The problem can be worked around either by
using syntax-case, or by
using syntax-rules but not (as much) CPS.
From this collaboration, I got an upper bound of 4 on my Erdős number: Paul Erdős > Paul T. Bateman > Eugene E. Kohlbecker > Daniel P. Friedman > Lindsey Kuper. This work was presented at the 2009 Scheme Workshop. [pdf]
My husband, Alex Rudnick, is a computational linguist working with the HLTDI and CNetS groups here at IU. We like to run marathons and pursue various side projects together.