[logo suggestions welcome]


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.

Mechanizing Metatheory Using Twelf

Robert Harper (Carnegie Mellon University)

What does it mean for a programming language to exist?  The usual
approach is to define a language by a "reasonably precise" description
a la K&R, together with a "reference compiler" that implements it (and
serves as the final arbiter of ambiguities).  This relies heavily on
social constructs such as standardization committees, or on the
marketing clout of a large corporation, and is not suitable as a basis
for a rigorous analysis of the safety or security properties of the

Another approach is to define a language by a rigorous semantics that
is amenable to mathematical analysis.  The most successful method of
semantic definition is to give a static semantics in the form of a
type system and a dynamic semantics in the form of execution rules for
a program.  This gives the definition an objective character that is
amenable to analysis, and helps to ensure the compatibility of
compilers for it.  But having a rigorous definition is not enough; at
a minimum one must prove that it is internally coherent according to
various criteria.  This re-introduces some of the difficulties of the
traditional methods, because someone has to do the proofs and someone
has to read them to ensure they are right.  The burdens of doing "at
scale" are so severe that the semantics becomes an inhibitor, rather
than an enabler, of innovation.

One way forward is to formalize the definition within a logical
framework and to use verification tools to check crucial properties,
much as we use type systems to ensure sensibility of our programs.  I
will describe the work we have been doing on mechanizing formal
language definitions, and describe some of the successes, and
difficulties, of using the Twelf system to verify their metatheory.

Joint work with Karl Crary and Michael Ashley-Rolman.

A Functional Approach to Typed Object-Oriented Programming

Rui Shi, Chiyan Chen, and Hongwei Xi (Boston University)

ATS is a recently developed programming language with a 
highly expressive type system rooted in the framework Applied Type System. 
In this paper, we present a design to support typed object-oriented 
programming (OOP) with multiple inheritance in ATS. In contrast to 
most existing approaches that represent objects as records, we instead 
represent objects as functions in ATS. We demonstrate that full-fledged 
support for OOP can be built directly on the top of the functional core 
of ATS without seeking ad hoc extensions. In particular, we show 
that a variety of issues with OOP (e.g., binary methods, the self type, 
parametric polymorphism, multiple inheritance) can be readily addressed 
by the approach we take to support OOP. 

For more information about ATS and the implementation, see http://www.cs.bu.edu/~hwxi/ATS/ATS.html.

Static Deadlock Detection for Java Libraries

Amy Williams, William Thies, and Michael D. Ernst (MIT)

Library writers wish to provide a guarantee not only that each
procedure in the library performs correctly in isolation, but also
that the procedures perform correctly when run in conjunction.  To
this end, we propose a method for static detection of deadlock in Java
libraries.  Our goal is to determine whether client code exists that  
may deadlock a library, and, if so, to enable the library writer to   
discover the calling patterns that can lead to deadlock.

Our flow-sensitive, context-sensitive analysis determines possible
deadlock configurations using a lock-order graph.  This graph
represents the order in which locks are acquired by the library.
Cycles in the graph indicate deadlock possibilities, and our tool
reports all such possibilities.  We implemented our analysis and 
evaluated it on 18 libraries comprising 1245 kLOC.  We verified 13
libraries to be free from deadlock, and found 14 distinct
deadlocks in 3 libraries. 

This work will be presented at ECOOP 2005. The full paper is available at http://cag.csail.mit.edu/~amy/papers/deadlock-ecoop05.pdf.

Debugging Concurrent Software by Context-Bounded Analysis

Shaz Qadeer (Microsoft Research)

Designing concurrent programs is difficult. The nondeterministic
interaction between concurrently executing threads of a concurrent
program results in programming errors that are notoriously difficult
to reproduce and fix. I will present a new static analysis technique
based on model checking for automatically finding errors in concurrent

An execution of a concurrent program is a sequence of contexts, where
each context consists of transitions performed by a single thread. My
work is motivated by the insight that many subtle errors in a
concurrent program are manifested by executions with few contexts. I
will use this insight to create analyses based on systematic state
exploration that are efficient and effective in finding concurrency

I will first present KISS (Keep It Simple and Sequential), a technique
for transforming a concurrent program P into a sequential program Q
that encodes all executions of P with a small number of contexts. I
used KISS to convert SDV (Static Driver Verifier), a model checker for
sequential C programs, into a model checker for concurrent C programs.
The combination of KISS and SDV has found a number of subtle
concurrency errors in Windows device drivers.

Next, I will present a new theoretical result which illustrates that
context-bounding significantly reduces the complexity of verifying
concurrent programs. It is well-known that the problem of verifying
assertions in a concurrent boolean program is undecidable. I will show
that if analysis is limited to executions with a fixed but arbitrary
context-bound, the problem becomes decidable, even in the presence of
unbounded dynamic thread creation.

This talk presents work done in collaboration with Dinghao Wu (Princeton University) and Jakob Rehof (Microsoft Research). Our two papers on this work, "KISS: Keep it simple and sequential" and "Context-bounded model checking of concurrent software" can be found at my home page under the heading "Recent Publications".

Exploiting Schemas in Data Synchronization

Nate Foster (University of Pennsylvania)

Increased reliance on optimistic data replication has led to
burgeoning interest in tools and frameworks for synchronizing
disconnected updates to replicated data. We have implemented a generic
synchronization framework, called Harmony, that can be used to build
state-based synchronizers for a wide variety of tree-structured data
formats. A novel feature of this framework is that the synchronization
process---in particular, the recognition of conflicts---is driven by
the schema of the structures being synchronized.  In this talk, I will
describe Harmony's core synchronization algorithm, state a simple and
intuitive specification, and illustrate how it can be used to build a
robust synchronizer for browser bookmarks.

Facilitating Pointer Program Verification with Stateful Views

Dengping Zhu and Hongwei Xi (Boston University)

A great obstacle in the verification of programs involving pointers is the
lack of an effective approach to modeling the highly dynamic nature of the
imperative data structures (e.g., various linked lists and trees) that make
explicit use of pointers.

In this talk, we show that (recursive) stateful views, a recently developed
type-theoretic notion for modeling memory layouts, can enable us to
effectively capture (sophisticated) invariants in pointer-rich programs
while retaining practical type-checking. For instance, the interesting
invariant can be readily captured in our system that each node in a doubly
linked binary tree points to its children that point back to the node
itself.  This is done in a programming paradigm which we call programming
with theorem proving.  We are to first briefly explain the type theory
behind stateful views and then present some realistic programming examples
based on a running implementation, which is currently available to the
public, to demonstrate the effectiveness of stateful views in facilitating
program verification involving pointers.

Our paper on this work can be found at ATS Homepage.

Quantifying the Performance of Garbage Collection vs. Explicit Memory Management

Matthew Hertz and Emery D. Berger (University of Massachusetts Amherst)

Garbage collection yields numerous software engineering benefits, but
its quantitative impact on performance remains elusive. One can
measure the cost of conservative garbage collection relative to
explicit memory management in C/C++ programs by linking in an
appropriate collector. This kind of direct comparison is not possible
for languages designed for garbage collection (e.g., Java), because
programs in these languages naturally do not contain calls to
free. Thus, the actual gap between the time and space performance of
explicit memory management and precise, copying garbage collection
remains unknown.

We describe a system we developed which enables us to take the first
steps towards quantifying the performance of precise garbage
collection versus explicit memory management. Using this "oracular"
memory management system, we compare explicit memory management to
both copying and non-copying garbage collectors across a range of
benchmarks. We then present results which quantify the time-space
tradeoff of garbage collection and show when garbage collection
performance is competitive with that of explicit memory management. We
also show that the time-space tradeoff for garbage collection is even
more observable when physical memory is scarce: while paging, garbage
collection can run over an order of magnitude slower than explicit
memory management.

Sneaking Existentials into Java

Kim Bruce (Williams College -> Pomona College via UCSC)

Existential types were introduced by Mitchell and Plotkin to model the sort
of abstraction found in abstract data types.  Existential types also play
an important role in hiding the visibility of instance variables in
modeling objects in object-oriented languages, though they are used quite
differently in modeling objects compared to ADT's.

Theoretically, existential types are quite nice, forming a nice dual to
universal (polymorphic) types, and supporting the Curry-Howard isomorphism
between types and formulas of inuitionistic second-order propositional

Wild-card types were a last minute addition to Java 5.  In fact, a minor
variant was rejected by the group controlling the evolution of the
language.  In this talk we review the use of existential types and how they
explain some of the idiosyncracies of wild-card types.  We also point out
how most of the uses of existential types could easily be eliminated from
the signatures of methods of Java libraries, though at some cost in verbosity.

Last modified Tuesday, June 14th, 2005 2:26:54pmPowered by PLT