New England Programming Languages and Systems Symposium Series (NEPLS): Abstracts

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.