These abstracts are for talks at this event.
NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.
The Future Is Parallel: What's a Programmer to Do?
Breaking Sequential Habits of Thought
Guy Steele (Sun Microsystems Laboratories)
Parallelism is here, now, and in our faces. It used to be just the supercomputers and servers, but now multicore chips are in desktops and laptops, and general practitioners, not just specialists, need to get used to parallel programming. The sequential algorithms and programming tricks that have served us so well for 50 years are the wrong way to think going forward. In this talk we illustrate the divide-and-conquer strategy with some small, cute, slightly surprising programs that represent the necessary future approach to program structure for program portability among parallel computational environments.
Screaming Fast Declarative Pointer Analysis
(Look Ma, no BDDs!)
Martin Bravenboer and Yannis Smaragdakis (University of Massachusetts)
We present the Doop framework for points-to analysis of Java programs. Doop builds on the idea of specifying pointer analysis algorithms declaratively, using Datalog: a logic-based language for defining (recursive) relations. We carry the declarative approach further than past work by describing the full end-to-end analysis in Datalog and optimizing aggressively through exposition of the representation of relations (e.g., indexing) to the Datalog language level. As a result, Doop achieves stunning (full order-of-magnitude) improvements in runtime. We compare Doop with Lhotak and Hendren's Paddle, which defines the state of the art for context-sensitive analyses. For the exact same logical points-to definitions (and, consequently, identical precision) Doop is 12.9x faster than Paddle for a 1-call-site sensitive analysis of the DaCapo benchmarks, and 10.2x faster than Paddle for a 1-object-sensitive analysis. At the same time, our implementation is modular and can be easily configured to analyses with a wide range of characteristics, largely due to its declarativeness.
For more information on this project, see the Doop website.
Putting Functions into Functional Programming
Shriram Krishnamurthi (Brown University)
Every middle-schooler knows that there are numerous representations for functions. The National Council of Teachers of Mathematics (NCTM), for instance, hopes that students at that level can "represent, analyze, and generalize a variety of patterns with tables, graphs, words, and, when possible, symbolic rules". Perhaps functional languages could support functions more comprehensively? Joint work with Danny Yoo, Emmanuel Schanzer, Kathi Fisler, and Matthias Felleisen.
Certified Systems Development in Ynot
Ryan Wisnesky and Gregory Malecha (Harvard University)
We describe our experience building a provably correct (certified) web-based course gradebook application in Ynot, an imperative programming library for Coq. We demonstrate that Ynot can be used to implement certified systems in a way similar to writing ML or Haskell code, including use of effectful, imperative features such as pointers, files, and socket I/O. The proof of system correctness is developed interactively with the programmer, imposes no runtime overhead, and can be verified in minutes by a several hundred-line typechecker. Ynot can be thought of as dependently typed Haskell with an IO monad that is indexed by pre and postconditions in the style of Hoare logic. Memory effects are reasoned about using separation logic, and we extend Ynot by adding support for reasoning about externally observable events like network and file I/O using a trace semantics. We demonstrate how certification of high level properties like privacy guarantees can be effectively isolated from certification of low level properties like memory safety and parsing correctness by leveraging higher-order functions and Coq's proof-search language.
Joint work with Greg Morrisett (Harvard University). The Ynot website can be found here.
The Extraordinary Algebra of List Comprehensions
Jan-Willem Maessen (Sun Microsystems Laboratories)
The Fortress programming language uses comprehensions and reductions as a compact notation for parallel operations that traverse multiple data structures and yield a single result. The literature on comprehensions is dominated by treatments of list comprehensions, and languages that provide comprehensions usually restrict both the type of the data structures that are traversed and the type of the result of the comprehension. Past efforts to generalize comprehensions show just how general and powerful the algebra of ordered sequences can be. However, this has often led to contradictory assumptions of what comprehensions should be and how they should work: for example, ordered sequences have monadic structure, but not every sequence type is necessarily a monad, and most monads aren't collections. In this talk we'll briefly tour the algebra of lists and explain the theory of comprehensions that we have chosen for the Fortress programming language.
More information on Project Fortress can be found on the Project Fortress Community Wiki and on the Sun Labs Programming Language Research Group Home Page. The talk slides are on-line.
Intrusion Detection for Ajax Applications
Arjun Guha (Brown University)
This is joint work with Shriram Krishnamurthi and Trevor Jim. The corresponding WWW 2009 Security Track paper is available online.
Synthesizing Robustness in Log Processing Programs
Jean Yang and Armando Solar-Lezama (MIT)
Missing or corrupted data is the bane of log-processing applications. Robust implementations in this domain establish policies for coping graciously with missing data, but robustness comes at a price: relatively simple common-case functionality is obscured by the complex logic required to enforce the policies. This talk introduces a new approach to this problem based on localized software synthesis. The goal is to synthesize a robust implementation from a brittle program together with its policy for coping with missing data or corrupted data. Our approach uses a combination of symbolic and concrete execution to discover the correct behavior in the presence of missing data, and then uses localized synthesis to modify the original program to adhere to this behavior. The talk will describe our programming model, and some of our preliminary results in this effort.
|Last modified Thursday, February 26th, 2009 11:27:10am|