[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.


Design and Research

Paul Graham

What happens when you treat programming languages as a design
problem instead of a research topic?  What do you do differently
when building a programming language is like designing a chair,
or a building, or a new typeface?   Ultimately I think research
and design converge.  If so, for programming language researchers,
this talk will be a description of what the target looks like
from the back.


Serving the Web

Paul Graunke (Northeastern University), Robert Bruce Findler (University of Chicago), Shriram Krishnamurthi (Brown University), Matthias Felleisen (Northeastern University)

The Web, originally designed for static content, now contains large
amounts of dynamically generated content.  The increase in flexibility
afforded by Web browsers strains most methods of constructing Web
software, leading to many defects.

In order to understand and address these defects, we construct a model
of the Web.  Our model captures several kinds of defects.  First, Web
programs interact with each other through Web forms.  Current Web
systems fail to prevent programs from attempting to extract
non-existent fields from Web forms.  Second, the nature of the HTTP
protocol interferes with updating pages once sent to the client.
These outdated pages lead consumers to make misinformed decisions
which the server interprets in the context of an incompatible state,
leading to disaster.

My talk will also present an overview of all of our Web development
tools, the shortcomings exposed by our model, and how we address them


Rigorously Modelling and Analyzing Hybrid Systems using Analytic Constraint Logic Programming

Tim Hickey (Brandeis University)

We use an interval-based Analytic Constraint Logic Programming (ACLP)
language to accurately and declaratively model highly non-linear
ODE-based Hybrid Systems.  The use of ACLP allows one to introduce
variables representing real valued functions and to constrain them
using functional equations. This provides a rigorous and declarative
model for Hybrid systems in which the behavior of the ACLP program
precisely mirrors the (theoretical) behavior of the Hybrid system.
One potential advantage of this approach is that program analysis
tools developed to analyze ACLP programs should automatically provide
tools for analyzing Hybrid systems. In this talk we describe the ACLP
framework, demonstrate how it can be used to model Hybrid systems, and
discuss the correspondence between program analysis tools and Hybrid
system analysis tools.


DrJVM: Safe, Efficient Support for Dynamic Class Upgrades in Java

David Reiss, Gregory Cooper, and Shriram Krishnamurthi (Brown University)

Software systems often require upgrades, both to fix bugs and to add
new features.  Upgrades traditionally consist of new libraries and
executables, which take effect only after the user restarts the
system.  In some applications, however, shutting a system down is
infeasible, and in such cases, users require the ability to upgrade
code within a running system.  While researchers have investigated
ways of implementing this capability, existing work suffers from
various weaknesses, including loss of static type safety,
inconvenience to the programmer, or performance degradation.  In this
talk, we present DrJVM, an implementation of the Java Virtual Machine
that supports dynamic upgrades in a type-safe, convenient, and
efficient manner.


Report on a Five Year Experiment in Teaching Web Programming in Scheme as a Computer Literacy Course

Tim Hickey (Brandeis University)

In this talk I will describe our use of Jscheme (a dialect of Scheme
implemented in Java) to teach the Computer Literacy course at Brandeis
over the past five years and will argue that using Scheme to teach web
programming allows one to be relevant in the student's eye's, while
still managing to cover important concepts in computation.


Language-Based Information-Flow Security

Andrei Sabelfeld and Andrew Myers (Cornell University)

Current standard security practices do not provide substantial
assurance that the end-to-end behavior of a computing system satisfies
important security policies such as confidentiality. An end-to-end
confidentiality policy might assert that secret input data cannot be
inferred by an attacker through the attacker's observations of system
output; this policy regulates information flow.

Conventional security mechanisms such as access control and encryption
do not directly address the enforcement of information-flow
policies. Recently, a promising new approach has been developed: the
use of programming-language techniques for specifying and enforcing
information-flow policies. This talk is intended to give the big
picture of recent and current research on information-flow security,
particularly focusing on work that uses static program analysis to
enforce information-flow policies.

Speaker's Supplement

The talk is based on a recent survey article (to appear in IEEE J-SAC) written jointly with Andrew Myers, available via http://www.cs.cornell.edu/~andrei/Papers/jsac.ps.


Implementing Staged Computation

Chiyan Chen and Hongwei Xi (Boston University)

Staged computation is a key to partial evaluation and run-time code
generation.  In this talk, we present a novel approach to implementing
staged computation through the use of guarded recursive (g.r.) datatype
constructors.  We first show how the notion of code can be captured with
g.r. datatype constructors and then present rules for typing and
translating staged programs, written in the MetaML-like syntax, into
ML-like programs that are typable in ML extended with g.r. datatype
constructors (ML_gr).

Compared to MetaML, our approach has the following advantages:

1. Staged programming can be completely embedded to ML_gr.  As a
consequence, we get free dynamic semantics for staged programming, as
provided by ML_gr.  Also, some difficult concepts in MetaML (e.g., the
built-in functions such as "run" and "lift") are provided with a simple
and natural explanation.  Moreover, with our type-preserving translation, we
also get free soundness (subject reduction) property of the typing for
meta-ML style stage programming.

2. Our staged programming offers more expressiveness than MetaML: Some
functions that are difficult or even impossible to stage in MetaML can be
staged with our approach.

3. Our type system of staged programming is stronger than that of MetaML.
In particular, we can readily differentiate open code from closed code,
and thus can statically prevent open code from being executed.

We also provide realistic examples in support of this simple and effective
approach to staged computation, which can readily be made available in
practice.


Decomposing lambda: the Kernel programming language

John N. Shutt (Worcester Polytechnic Institute)

The Kernel programming language attempts to expand on the simplicity and
versatility of Scheme by exploiting a decomposition of Scheme's lambda
constructor into two orthogonal constructors.  The primary constructor,
called $vau, builds compound combiners that act directly on their unevaluated
operands ("call-by-text"); while a second constructor, called simply "wrap",
induces evaluation of arguments.  This talk explains how these constructors
work, and explores some of their consequences.  Using the new constructors,
a variety of core Scheme primitives may be constructed as Kernel compound
combiners --- notably including $lambda, apply, $quote, and (incidentally)
car and cdr.  The capabilities of macro facilities are entirely subsumed.
Kernel also incorporates several design differences from Scheme that help
the programmer to manage the inherent volatility of first-class call-by-text
compound combiners.  Several past LISP languages have included devices
similar to $vau (such as the notorious "FEXPRs") but did not offer sufficient
means to manage the accompanying volatility.  The talk describes several of
Kernel's management-motivated deviations from Scheme, ranging from overt
syntax to subtle semantics.


Computational Soundness of Non-Confluent Calculi

Elena Machkasova (Wellesley College)

Traditionally, there are two ways of reasoning about a program: a small 
step operational semantics that defines the meaning of a program and 
a calculus rewrite relation that describes program transformations. 
Computational soundness connects these two; it implies that any 
transformation expressible in the calculus preserves meaning with respect
to the small-step operational semantics. The usual technique for proving  
computational soundness is based on confluence and standardization. 
However, this approach is not applicable to many calculi
because of lack of confluence. 

In this talk I will give a brief overview of the traditional approach to 
computational soundness proofs and describe a technique for proving 
computational soundness which does not require confluence of the calculus. 
The technique is based on two properties, lift and project, introduced
in Machkasova and Turbak ``A Calculus for Link-time Compilation''.
I will focus on a proof of these properties in the case of a small 
calculus of records with mutually recursive components. In addition
to lacking confluence, this calculus does not have other properties 
commonly used in computational soundness proofs, such as left-linearity 
and finiteness of developments. However, we are able to show that the 
calculus is computationally sound. 


The MulSaw Approach to Automated Specification-Based Testing

Darko Marinov and Sarfaz Khurshid (MIT)

This talk presents two complementary frameworks that the MulSaw
project has developed for automated specification-based testing of
Java programs.  Both frameworks test a method by first generating all
nonisomorphic inputs (within a given input size) that satisfy the
method precondition and then executing the method on each input and
using the method postcondition as a test oracle for checking the
correctness of each output.

The first framework allows programmers to write specifications in
Alloy, a first-order, relational language.  This framework translates
a precondition into a boolean satisfiability formula and uses an
off-the-shelf SAT solver to enumerate solutions to the formula; these
solutions correspond to nonisomorphic test inputs.  The second
framework allows programmers to write specifications using Java
expressions.  This framework provides a novel algorithm for generation
of nonisomorphic inputs for which the Java predicate that corresponds
to a precondition returns true.

We have used these frameworks to test several Java programs, including
data structure implementations from the Java Collections Framework, a
naming architecture for mobile networks, and the Alloy Analyzer (AA).
For data structures, the experimental results indicate that it is
feasible to systematically generate inputs that achieve complete
statement and branch coverage.  For the naming architecture and AA,
this systematic testing revealed subtle errors.

Speaker's Supplement

Details of the MulSaw project can be found online at http://mulsaw.lcs.mit.edu.


Last modified Friday, October 11th, 2002 1:31:59pmPowered by PLT