![[logo suggestions welcome]](/logo.gif){kind=logo}
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.
Call-By-Push-Value: A Subsuming Paradigm
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/.
