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)

Browser-based applications are gaining popularity as technologies like
Ajax mature and browsers become more powerful platforms. However, Ajax
applications remain notoriously difficult to write and harder still to
write securely. In addition to the standard security challenges that
face web applications, Ajax applications must contend with a host of
new issues, such as foreign script injection and a programming
environment with very few static guarantees.

We use static program analysis of JavaScript and HTML to automatically
generate a sound model of an Ajax application's interactions with its
server. We construct a lightweight proxy that ensures that clients do
not violate the model. We efficiently insert random requests into
clients on a per session basis, introducing a degree of randomness
into each model. This makes it harder to construct a generic attack
that defeats a generic model. Finally, we evaluate our tools and
techniques against real web applications.

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