![[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.
Bottom-up beta-reduction: uplinks and lambda-DAGs
Olin Shivers (Georgia Institute of Technology)
Thoughts on Subtypes vs. Inheritance
Kim Bruce (Williams College)
As long ago as the mid-1980's, language researchers recognized that subtyping and inheritance were different concepts. Yet nearly all popular object-oriented languages have conflated the two concepts. My recent research (discussed at NEPLS in the summer of 2002) on simultaneous specialization of mutually recursive classes has helped me understand better the differences between these two concepts. In this talk I will discuss these differences and highlight the differences using examples involving multiple classes and types. While my thoughts are based on research in types and semantics, the points that I want to make are more conceptual or even philosphical.
My paper, Some challenging typing issues in object-oriented languages, provides an overview of problems related to simultaneous specialization of mutually recursive collections of classes.
Which Security Policies Can Rewriters Enforce?
Kevin Hamlen (Cornell University)
Modern software must balance the purveyance of desired program behaviors (features) with the prohibition of unacceptable behaviors. Opportunities to protect against such unacceptable behaviors arise both prior to program execution and during execution. Checking an untrusted program prior to execution requires a static analysis that accepts or rejects the program in finite time. Accepted programs are then executed without restriction while rejected programs are not run at all. In contrast to static analyses, Execution Monitors (EM's) protect against unacceptable program behaviors by monitoring untrusted programs as they execute. If the untrusted program attempts to perform an unacceptable action, it is halted or some other corrective action is taken. Work by Schneider has shown that Execution Monitors can enforce only security policies that are safety properties. We consider a third class of security policies: those that can be enforced by a program-rewriter. A program-rewriter modifies a program before it is executed so that (1) the rewritten program always satisfies the desired security policy, and (2) if the original program already satisfied the security policy, the rewritten program's behavior is semantically equivalent to the original's. We show that program-rewriters can enforce security policies that are not enforceable by any Execution Monitor. In addition, we show that Execution Monitors cannot enforce all safety properties. Rather, they can only enforce those safety properties that are also enforceable by program-rewriters. The result of our analysis is a taxonomy of enforceable security policies.
This talk presents work done in collaboration with Greg Morrisett (Harvard University) and Fred Schneider (Cornell University). A tech report version of our paper can be found here.
TStreams, a New Language for Parallel Computation
Carl Offner (HP Cambridge Research Lab)
Current languages for parallel programming have the following characteristics: * They specify particular parts of a program that can be executed in parallel. Any other parts are not assumed to be parallel. * The type of parallelism supported by each language is specific to that language. For instance, it may be data parallel or task parallel. In contrast, TStreams provides a way of specifying the inherent constraints on parallelism in a program. There is only one kind of constraint: all producer-consumer relations must be honored. Any computations not ordered by these constraints can be executed in parallel. In this way, TStreams represents all forms of parallelism in a program (including, for instance, pipelined parallelism) without regard to the target architecture. TStreams therefore gives the programmer the ability to express a parallel algorithm in its most natural form. TStreams can be viewed as a combination of functional programming, tuple spaces, and streaming, but with important differences from each. TStreams can be viewed either as a language which the programmer can write in directly, or as an intermediate form which is generated from ordinary serial code in any conventional language. TStreams form can either be interpreted directly or compiled into code targeted to arbitrary parallel architectures. In our current prototype the programmer writes in TStreams, the TStreams code is interpreted, and the TStreams interpreter runs on a cluster of SMPs. Joint work with Kath Knobe (HP Cambridge Research Lab) and Alex Nelson (HP High Performance Technical Computing).
Example-Centric Programming
Jonathan Edwards (Massachusetts Institute of Technology)
One reason programming is so hard is that programs are intricate abstractions. We best learn and understand abstractions through examples. Accordingly when we read or write code we often have in mind specific examples of how it will execute. This research seeks to make these examples explicit and concrete within an IDE, leveraging the abstraction capabilities of programmers, and making programming easier. Unit tests are a good source of examples. Even lighter-weight examples can take the form of snippets of code making calls. The basic idea is to instrument and execute these examples in the background and use the resulting trace to illuminate the source code within the editor. Two visual metaphors are being explored: directly annotating values into the source view itself; and a tree browser of the execution trace that is synchronized with the source editor. The illusion that the entire execution history is browsable in arbitrary detail is supported by re-instrumenting and re-executing on demand. The ideal is that all code is illuminated by some example, and that one never needs to leave this example-enlightened code editor. The exploration made possible by REPL shells is subsumed in this interface. Unit testing is also subsumed and made automatic. Debugging of examples and tests can be done without leaving the editor, just by browsing and inspecting. Eliminating the need to mode-switch into these other tools may improve the workflow of programming. Examples may be decorated with _assertions_ that freeze the current value of an expression and henceforth check that it remains the same. This allows examples to grow into unit tests without coding. Examples may also be decorated with _assumptions_ that force an expression to take a value. This allows externalities to be simulated without complex mock-up code. These assertions and assumptions can be applied to an arbitrary expression in an arbitrary call in the execution trace of an example. This supports intrusive testing, probing into the internals of the code to insert test values and check test results. A research question is how well such deep tests serve as a kind of scaffolding within which programs are constructed. This research may cast new light on the old debate between static and dynamic types. Static types catch some errors at compile-time and also provide semantic assistance in the IDE (e.g. call-tips). Examples can largely provide the same benefits even with dynamically typed languages. Actual execution instances being available at "edit-time" vitiates the compile-time/run-time dichotomy at the heart of type systems. A prototype is being implemented for Java in the Eclipse IDE. This will be demonstrated, accompanied by hand-waving over the unfinished parts.
Reintroducing Modules into an Object-Oriented Language
Christopher Diggins
In several object oriented programming languages, certain older effective software design techniques have been abandoned but then reintroduced indirectly through other new features which are perhaps less appropriate. In this talk we use the Heron programming language to show how by re-introducing a module construct into an object oriented programming language we can simplify the complexity of objects and classes.
For an outline of the talk, see http://www.heron-language.com/modular-programming.html.
More information on the Heron language, including an informal specification, can be found at http://www.heron-language.com
Exploiting Purity for Atomicity
Stephen Freund (Williams College)
The notion that certain procedures are atomic is a fundamental correctness property of many multithreaded software systems. A procedure is atomic if for every execution there is an equivalent serial execution where the actions of the atomic procedure are not interleaved with actions of other threads. Several existing tools verify atomicity by showing that every execution reduces to a corresponding serial execution. However, experiments with these tools have highlighted a number of interesting procedures that, while intuitively atomic, are not reducible. In this talk, we exploit the notion of pure code blocks to verify the atomicity of such irreducible procedures. If a pure block terminates normally, then its evaluation does not change the program state, and hence these evaluation steps can be removed from the program trace before reduction. We develop a static analysis for atomicity based on this insight, and we illustrate this analysis on a number of interesting examples that could not be verified using earlier tools based purely on reduction. These techniques may also be applicable in other approaches for verifying atomicity, such as via software model checking or dynamic analysis.
This is joint work with Cormac Flanagan (University of California, Santa Cruz) and Shaz Qadeer (Microsoft Research). For more information on this project, see our atomicity web page.
Programming Examples Needing Polymorphic Recursion
J. J. Hallett (Boston University)
Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type inference for polymorphic recursion using forall-types has been proved undecidable. This report presents several programming examples involving polymorphic recursion and determines their typability under various type systems, including the Hindley-Milner system, an intersection-type system, and extensions of these two. The goal of this report is to show that many of these examples are typable using a system of intersection types as an alternative form of polymorphism. By accomplishing this, we hope to lay the foundation for future research into a decidable intersection-type inference algorithm. We do not provide a comprehensive survey of type systems appropriate for polymorphic recursion, with or without type annotations inserted in the source language. Rather, we focus on examples for which types may be inferred without type annotations, with an emphasis on systems of intersection-types.
This talk presents work done in collaboration with Assaf Kfoury (Boston University). Our paper on this work can be found at The Church Project.
Encoding Regions
Matthew Fluet (Harvard University)
The region calculus, first introduced by Tofte and Talpin, has a fairly complicated type-and-effects system that is used to ensure that pointers into deallocated storage are never dereferenced. In a separate line of research, Launchbury and Peyton-Jones introduced monads as a mechanism by which imperative (and otherwise "effectful") constructs can be safely integrated into pure functional languages. We demonstrate that the type system of the region calculus can be encoded in the polymorphic lambda calculus augmented with monadic types and operations. The encoding is based upon a generalization of the ST monad and likewise presents an encapsulation operator whose parametric type ensures that regions (and values allocated therin) are neither accessible nor visible outside the appropriate scope.
This paper appeared in SPACE'04 and is available from the workshop website: http://www.diku.dk/topps/space2004/
Relating Backtracking Monads
Dale Vaillancourt (Northeastern University)
There are two well-known models of backtracking computation: the stream model and the two-continuation model. The stream model treats backtracking computations with a stream of possible answers, and the two-continuation model uses a success continuation and a failure continuation. Hughes [2000] defined a "backtracking monad" to be a monad with additional operations "disj" and "fail" satisfying 5 additional axioms. Both the stream model and the two-continuation model are backtracking monads, but this fact does not give us any deeper relation between the two. Past attempts to relate these models have met with limited success: either the types do not work out, or the relation works in one direction but not the other, or the relation does not work for higher-order values. We show how to relate the monads in a simple way. We relate streams of scalars using a representation inspired by Danvy et al. [2001]. We then extend this to higher-order values using logical relations. At observable types this turns into the identity relation, so we get a denotational equivalence between the values in each model. All of this is done with only elementary mathematics; no category theory is necessary!
This talk presents work done in collaboration with Mitchell Wand (Northeastern University).
Enforcing Static Access Control with Guarded/Asserting Types
Sa Cui (Boston University)
Access control is a security mechanism to protect resources of the
local system from untrusted agents. The Java Security Architecture
(JSA) provides a dynamic mechanism to support access control by
performing stack inspection at run-time. In contrast to JSA, there
are also approaches that have been proposed to support access
control statically, which can avoid potentially high run-time
overhead of stack inspection. For instance, in the type system of
$\lambda_{SEC}$, certain access control policies can be enforced
through statically type checking.
In this paper, we propose an approach to supporting static access
control through the use of guarded and asserting types. The notion
of guarded and asserting types can be traced back to the work on
restricted form of dependent types (as is developed in DML) and
guarded recursive datatypes. This notion has since been formalized
in the framework Applied Type System (ATS). We show that guarded
and asserting types can also be used in a natural manner to cope
with the issue of static access control. In particular, we are to
translate $\lambda_{SEC}$ into a calculus that essentially extends
simply typed lambda calculus with guarded and asserting types.
Intersection Types: Idempotent is Potency
Peter Neergaard (Brandeis University)
Intersection type systems realize a finite polymorphism where the different typings for a term are itemized explicitly (as a contrast to the parametric polymorphism of ML and Haskell). We analyze System I which is a prototype system developed as part of the Church project. It embodies an intersection type system with a strict intersections---they lack associativity, commutativity, and idempotent, i.e., a /\ (b /\ c) <> (a /\ b) /\ c, a /\ b <> b /\ a, and a /\ a <> a. It also employs the novel technology of expansion variables to facilitate modular program composition and flow analysis. We establish two interesting results: - we draw a tight connection between intersection types and linear logic and interaction nets. - we prove that the problem of type inference is always synonymous with normalization: the normal form can be obtained from the principal typing and vice versa. Type inference is thus as costly as running the program. The key to this result is that simply-typed terms must be linear without idempotent. We note that with idempotent (and associativity and commutativity), we regain the usual nonelementary power of simply-typed terms. For programming language people the conclusion is that idempotent (which is usually present in typed programming language) is crucial for type inference being faster than running the program.
