[logo suggestions welcome]

N
E
P
L
S

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.


Modules with Interfaces for Dynamic Linking and Communication

Scott Smith (The Johns Hopkins University)

Module systems are well known as a means for giving clear interfaces
for the static linking of code.  This talk describes how adding
explicit interfaces to modules for 1) dynamic linking and 2)
cross-computation communication can increase the declarative,
encapsulated nature of modules, and build a stronger foundation for
language-based security and version control.  We term these new
modules Assemblages.


Partial Evaluation for Shift and Reset

Kenichi Asai (Northeastern University)

In this talk, I describe partial evaluation of the lambda-calculus
with the delimited continuation constructs shift and reset.  After
illustrating the use of delimited continuations with examples, I
define the semantics of shift and reset in two ways: one by writing a
continuation-passing style (CPS) interpreter and the other by
transforming them into CPS.  It is then shown that a partial evaluator
can be simply obtained by combining them: static reduction is
performed as in the CPS interpreter and dynamic residualization is
performed as in the CPS transformer.

The obtained partial evaluator is online and produces the output in
CPS.  By transforming the partial evaluator back into a direct style
(DS), a partial evaluator producing the output in DS is obtained.  
Offline versions are similarly obtained by incorporating a type system
(due to Danvy and Filinski) that takes continuations into account.
The correctness proof for these partial evaluators is involved.  So
far, only one of the offline partial evaluators is proven correct.


A New Approach to Logic Programming with Names and Binding

James Cheney (Cornell University)

Fresh name-generation, alpha-equivalence, and capture-avoiding
substitution pose problems for most practical programming paradigms,
and logic programming is no exception.  Some of thse problems can be
solved by working in a higher-order logic programming language and
using higher-order abstract syntax (HOAS), that is, the technique of
using a meta-language's lambda-abstraction to encode all forms of
variable binding in an object language.  HOAS is supported in several
logic programming languages, often affords very clean and elegant
encodings, but is semantically complex and encodings are often very
different from informal presentations (i.e., what you would write in a
paper).  As a result, reasoning about the correctness and other
properties of HOAS encodings can be difficult.

Recently, Gabbay and Pitts discovered a new way of modeling abstract
syntax with names and binding that permits a style of programming that
is much closer to informal practice yet semantically much simpler than
HOAS.  I (together with Christian Urban, U. Cambridge) am developing a
logic programming language called alpha-Prolog which supports
programming using these new techniques.  In this talk I will describe
the approach, explain how alpha-Prolog programs run, and describe a
few examples.

For more information, see the project homepage.


Automatic Conversion of Java code to use Generic Libraries

Alan Donovan, Adam Kiezun, Michael Ernst (MIT)

The type system of Java 1.5 will include support for parametric
polymorphism, or generic classes.  This will bring many benefits to
Java programmers, not least because current Java practice makes heavy
use of logically-generic classes, including container classes, and
requires programmer discipline to make use of them in a type-safe
manner.

We present a technique to determine sound and precise parametric types
at each use of a class for which a generic type specification is
available.  Our approach employs a precise and context-sensitive
concrete class analysis to determine a type for each allocation site
of a generic container class based on what elements are stored in it;
and a type-constraint-based analysis to choose consistent types for
all the declarations in the input source code.

We discuss a number of subtle problems encountered in addressing all
of the features of the source and target languages, in particular, raw
types.  We have implemented our analysis in a tool, Jiggetai, that
automatically inserts type parameters into Java code, and we report
its performance when applied to a number of real-world Java programs.

This work will appear in OOPSLA'04. The paper will be available at this location.


Memory Conscious Object-Oriented Programs

Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin (National University of Singapore), and Martin Rinard (MIT)

We present a new (size-)polymorphic type system (for an
object-oriented language) that characterizes the sizes of data
structures and the amount of heap and stack memory required to
successfully execute methods that operate on these data
structures. Key components of this type system include type assertions
that use symbolic Presburger arithmetic expressions to capture data
structure sizes, the effect of methods on the sizes of the data
structures that they manipulate, and the amount of memory that methods
allocate and deallocate. For each method, it can provide expressions
that (conservatively) capture the amount of memory required to execute
the method as a function of the sizes of the method's inputs. The
safety guarantee is that the method will never attempt to use more
memory than its type expressions specify.

We have implemented a type checker for programs written with our type
system and used this checker to verify the memory usages for a variety
of programs. Our experience is that the type system can effectively
capture the memory system needs of our programs.


Path Grammars

Craig Damon (University of Vermont)

Path grammars represent a new mechanism for representing control flow
information within a program. Each executable unit, such as a
statement, an expression or a basic block, is represented by a letter
in the alphabet of the path language. The sentences in this language
represent all possible executions of the program. A superset of this
language, which ignores data dependencies, can be described by a
context free grammar, the path grammar.

Traditional control- and data-flow algorithms can be adapted to work
directly on the path grammar, with the same asymptotic performance
displayed by those algorithms working on a traditional control flow
graph. Replacing control flow graphs with path grammars offers several
advantages, including context-sensitivity, path manipulations and the
opportunity to describe portions of the possible execution.


Verifying Aspect Advice Modularly

Shriram Krishnamurthi (Brown University), Kathi Fisler (WPI), and Michael Greenberg (Brown University)

Aspect-oriented programming has become an increasingly important means
of expressing cross-cutting program abstractions.  Despite this,
aspects lack support for computer-aided verification.  We present a
technique for verifying aspect-oriented programs (expressed as state
machines).  Our technique assumes that the set of pointcut designators
is known statically, but that the actual advice can vary.  This calls
for a modular technique that does not require repeated analysis of the
entire system every time a developer changes an advice.  We present
such an analysis, addressing several subtleties that arise.


Hippocratic Garbage Collection

Matthew Hertz, Yi Feng and Emery Berger (University of Massachusetts)

Programs written in garbage-collected languages like Java often have
large working sets and poor locality. Worse, a full garbage collection
must visit all live data and is likely to touch pages that are no
longer resident, triggering paging. The result is a pronounced drop in
throughput and a spike in latency. We show that just a slight
reduction in available memory causes the throughput of the SPECjbb
benchmark to drop by 66% and results in garbage collection pauses
lasting for several seconds.

We introduce page-level cooperative garbage collection, an approach in
which the garbage collector works with the virtual memory manager to
limit paging. We present a novel, cooperative garbage collection
algorithm called Hippocratic collection. By communicating with the
virtual memory manager and ``bookmarking'' objects, the Hippocratic
collector eliminates paging caused by garbage collection. Our approach
requires only modest extensions to existing virtual memory management
algorithms. We present empirical results using our modified Linux
kernel showing that the Hippocratic collector runs in smaller
footprints than traditional collectors while providing competitive
throughput.

Our technical report on this work can be found at this location.


Last modified Monday, May 31st, 2004 9:15:03pmPowered by PLT