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. I received my MS in Computer Science from IU in 2010 and my BA in Computer Science and Music from Grinnell College in 2004. (CV: pdf, txt)
Deterministic parallel programming models guarantee freedom from difficult-to-reproduce nondeterministic bugs such as race conditions. Models of parallel programming that are deterministic by construction range from pure functional models, to domain-specific languages based on dataflow, to research languages that permit heavily annotated imperative programs. With Ryan Newton, I'm investigating how the determinism of each of these models hinges on a notion of monotonicity. Our goal is to develop a theory of monotonic data structures—data structures to which information is only added and never removed—that is expressive enough to guide and unify the development of new deterministic parallel models. 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]
I was fortunate to spend the spring and summer of 2011 working with a fantastic team at Mozilla Labs on the design and implementation of the Rust programming language. The original design of Rust 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 for a language that tries to statically guarantee type safety posed an interesting challenge, since dynamic object extension and method overriding cause the type of the current object to change at run-time. While at Mozilla I implemented self-dispatch, object extension, and method overriding in the original Rust object system and learned that these 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]
Work on Rust is ongoing; you can help! Join in the discussion on the rust-dev mailing list, or follow the progress on GitHub or Twitter.
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.