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.

What are Polymorphically-Typed Ambients?

Torben Amtoft and Assaf J. Kfoury and Santiago M. Pericas-Geertsen
Boston University

The Ambient Calculus was developed by Cardelli and Gordon as a formal
framework to study issues of mobility and migrant code. We consider an
Ambient Calculus where ambients transport and exchange programs rather
that just inert data. We propose different senses in which such a
calculus can be said to be polymorphically typed, and design
accordingly a polymorphic type system for it which assigns types to
embedded programs and what we call behaviors to processes.  The
subtyping relation on behaviors is semantic rather than axiomatic, in
that the denotation of a behavior is a set of traces.  Our
polymorphically-typed calculus satisfies a subject reduction property,
and is a conservative extension of the typed Ambient Calculus
originally proposed by Cardelli and Gordon.  Based on techniques
borrowed from finite automata theory, type-checking of fully
type-annotated processes is shown to be decidable.


#### Speaker's Supplement

Papers describing our work (a long as well as a short version) can be found at http://types.bu.edu/reports/.

Type-Preserving Compilation of Java

Christopher League
Yale University

We present an efficient encoding of core Java constructs in a simple,
implementable typed intermediate language.  The encoding, after type
erasure, has the same operational behavior as a standard
implementation using vtables and self-application for method
invocation.  Classes inherit super-class methods with no overhead.  We
support mutually recursive classes while preserving separate
compilation.  Our strategy extends naturally to a significant subset
of Java, including interfaces and privacy.

(joint work with Valery Trifonov and Zhong Shao)


#### Speaker's Supplement

My recent work is available as a draft; it has been accepted at the FOOL workshop in January. The following URL leads to the draft version for now: http://flint.cs.yale.edu/flint/publications/fjcomp.html. The final version will likely not be ready until just after NEPLS.

Paul Blain Levy
Computer Science Department
Boston University

Call-by-push-value (CBPV) is a new, typed programming language
paradigm that, we claim, provides the semantic primitives from which
the call-by-value and call-by-name paradigms are built.  Evidence for
this claim is found in a wide range of semantics, from operational and
machine semantics to denotational models such as domains,
continuations, possible worlds and games.  CBPV is based on work of
Moggi and Filinski.

In this talk, we introduce CBPV and use an example program to
illustrate the way that it combines functional and imperative features
using the slogan "a value is, a computation does".  We look at the
Scott semantics and at other computational effects such as global
store.


#### Speaker's Supplement

An extended abstract about call-by-push-value appears at http://www.dcs.qmw.ac.uk/~pbl/papers/tlca99.ps.gz.

Unfold/Fold Transformations of Logic Programs

Abhik Roychoudhury
SUNY Stony Brook

Unfold/fold transformations of logic programs are extensively used in
program synthesis, program optimization and proving program
properties.  However, any arbitrary sequence of these transformations
does not preserve program semantics since folding can introduce
circular dependencies in the program. To ensure correctness, existing
transformations restrict the syntax of the program clauses to which an
unfold/fold step is applied.

In this talk, we present a more general transformation framework which
relaxes these restrictions. We perform book-keeping with each
unfold/fold step and determine the applicability of the
transformations solely by this book-keeping (not by program syntax).
The transformations preserve the least Herbrand model semantics of
definite logic programs and the well-founded model / stable model
semantics of normal logic programs.  Existing transformation systems
are shown to be instances of our framework. Development of this
transformation framework is motivated by its use in proving temporal
properties of concurrent programs.


#### Speaker's Supplement

This paper appeared as

A Parameterized Unfold/Fold Transformation Framework for Definite Logic Programs, A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan and I.V. Ramakrishnan, International Conference on Principles and Practice of Declarative Programming (PPDP) 1999, LNCS 1702, pg 396-413.
and is available from http://www.cs.sunysb.edu/~abhik/papers/.

Programming and Compiling with Concepts

Sibylle Schupp
RPI

For abstract data types (ADTs) there are many potential optimizations
of code that current compilers are unable to perform.  These
optimizations either depend on the functional specification of the
computational task performed through an ADT or on the semantics of the
objects defined. In either case the abstract properties on which
optimizations would have to be based cannot be automatically inferred
by the compiler---they are not even available at compiler design time.

In this talk we show how to design a small optimization component, the
simplification component, so that it can be extended at compile time
of a user program. With the original data type designer providing a
description of a type's behavior, the compiler can operate on a strong
semantic base and, as a result, generate more efficient code. Key in
decoupling the process of simplification and the semantics of data
types is the \emph{concept-based} approach, a methodology that was
made popular by the Standard Template Library (STL) and is
increasingly used in the design of reusable software components and
software libraries, but has not previously been applied to compiler
design.

This is joint work with Douglas Gregor and David Musser.


Dynamic Partial Evaluation

Greg Sullivan
MIT

Dynamic partial evaluation performs partial evaluation as a side
effect of evaluation, with no previous static analysis required.  A
completely dynamic version of partial evaluation is not merely of
theoretical interest, but has practical applications, especially when
applied to dynamic, reflective programming languages.  Computational
reflection, and in particular the use of meta-object protocols (MOPs),
provides a powerful abstraction mechanism, providing programmatic
hooks'' into the interpreter semantics of the host programming
language.  Unfortunately, a runtime MOP defeats many optimizations
based on static analysis (for example, the applicable methods at a
call site may change over time, even for the same types of arguments).
Dynamic partial evaluation allows us to apply partial evaluation
techniques even in the context of a meta-object protocol.  We have
implemented dynamic partial evaluation as part of a Dynamic Virtual
Machine intended to host dynamic, reflective object-oriented
languages.  In this talk, I will present an implementation of dynamic
partial evaluation for a simple language -- a lambda calculus extended
with dynamic typing, subtyping, generic functions and multimethod
dispatch.


#### Speaker's Supplement

You can use http://www.ai.mit.edu/~gregs/dynamic-pe.html.

Scalable Propagation-Based Call Graph Construction Algorithms

Frank Tip
IBM Watson

Propagation-based call graph construction algorithms have been studied
intensively in the 1990s, and differ primarily in the number of sets
that are used to approximate run-time values of expressions. In
practice, algorithms such as RTA that use a single set for the whole
program scale well. The scalability of algorithms such as 0-CFA that
use one set per expression remains doubtful.

This presentation will consist of two parts. The first part consists
of a brief introduction to call graph construction for object-oriented
languages, and briefly reviews a number of well-known previous
algorithms such as Class Hierarchy Analysis (CHA), Rapid Type Analysis
(RTA), and 0-CFA. In the second part of the presentation, I will
present a number of new algorithms that fall in the design space
between RTA and 0-CFA. We have implemented these algorithms in the
context of JAX, an application extractor for Java, and shown that they
all scale to a 325,000-line program.  A key property of these
algorithms is that they do not analyze values on the run-time stack,
which makes them efficient and easy to implement. Surprisingly, for
detecting unreachable methods, the inexpensive RTA algorithm does
almost as well as the seemingly more powerful algorithms. However, for
determining call sites with a single target, one of our new algorithms
obtains the current best tradeoff between speed and precision.

This is joint work with Jens Palsberg (Purdue University).


#### Speaker's Supplement

The paper that I will be presenting recently appeared in the proceedings of OOPSLA'00. You can find an abstract on my home page: http://www.research.ibm.com/people/t/tip/.