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.

Integrating Testing with Theorem Proving in ACL2s

Harsh Raju Chamarthi (Northeastern University)

Using an interactive theorem prover to reason about programs involves
a sequence of interactions where the user challenges the theorem
prover with conjectures. Invariably, many of the conjectures posed are
in fact false, and users often spend considerable effort examining the
theorem prover's output before realizing this. We present a
lightweight method, implemented in the ACL2 Sedan (ACL2s), for
automatically generating concrete counterexamples. Our approach
automatically generates examples that are guaranteed to satisfy
hypotheses restricting the type of a variable. Furthermore, we use the
full power of the theorem prover to simplify conjectures, leading to a
very powerful, synergistic integration of testing with theorem
proving. We will discuss our experience with using ACL2s to teach
freshmen students how to reason about programs and will give a demo
that includes several examples.

This is joint work with Peter Dillinger, Matt Kaufmann and Panagiotis

Delimited Checkpoints for Effective Contracts

Avi Shinnar (Harvard University)

Delimited checkpoints are a convenient interface that we can use to
build effective contracts.  Like first class checkpoints, they allow a
form of time travel, letting a computation capture a snapshot of
memory and restore it at some later point.  Crucially, they also allow
for comparison operations, allowing a contract to determine the
footprint of a computation.  This allows us to build expressive
contracts, including framing contracts such as modifies and
post-conditions that can reference the pre-execution state of memory.
Additionally, they support assertions that are guaranteed to be
erasable, despite having local effects.

Observing that these contracts only require the use of checkpoints in
a delimited (region based) manner, we restrict our attention to
checkpoints that are only used within a given scope: hence "delimited"
checkpoints.  This allows for a simple implementation reusing the
mechanisms underlying Software Transactional Memory.  A prototype of
this system has been created by extending GHC's implementation of STM

Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints

Vasilis Papavasileiou (Northeastern University)

We present techniques that enable designers to algorithmically
synthesize cyber-physical architectural models with real-time
constraints. We do this by providing a declarative language that
allows designers to specify what properties their architectural models
should have, not how to achieve them. This provides designers with a
qualitatively new level of abstraction that enables the exploration of
design spaces at the earliest stages of design, when doing so provides
the most benefit. Our system was used to automatically synthesize
cyber-physical architectural models with hard real-time constraints
from a large-scale industrial design.

Macros that Oblige

Martin Hirzel (IBM Watson Research Center)

This talk describes two contributions:

1. Higher-order macros with contracts and hygiene.

2. Higher-order composite stream-processing operators with contracts.

Contribution (1) enables contribution (2), and contribution (2)
motivates contribution (1). But this talk explains (1) and (2)
separately to facilitate understanding and adoption.

Implicit Arrow Annotations in Alms

Jesse Tov (Northeastern University)

Alms is a practical language with affine types, but it is not quite as
practical as it could be.  One thing weighing it down is the need for
"usage" annotations on arrows. For most types, Alms infers how many
times values of that type can be used (freely or only once) from the
structure of the type, but in general, the domain and codomain of a
function type do not determine how many times the function can be
used. Thus, function arrows require annotation.

In the common case, however, arrow annotations follow regular
patterns, and are therefore predictable. We can exploit this
regularity to infer annotations on unadorned arrow types. In cases
where the default annotation would be wrong, an explicit annotation
can override it. The annotation inference rules have no effect on type
soundness, but a good heuristic minimizes the annotation burden while
making the implicit annotations predictable by the programmer.

Taming the Wildcards: Combining Definition- and Use-Site Variance

John Altidor (University of Massachusetts, Amherst)

Variance allows the safe integration of parametric and subtype
polymorphism. Two flavors of variance, definition-site versus use-site
variance, have been studied and have had their merits hotly
debated. Definition-site variance (as in Scala and C#) offers simple
type-instantiation rules, but causes fractured definitions of
naturally invariant classes; Use-site variance (as in Java) offers
simplicity in class definitions, yet complex type-instantiation rules
that elude most programmers.

We present a unifying framework for reasoning about variance. Our
framework is quite simple and entirely denotational, that is, it
evokes directly the definition of variance with a small core calculus
that does not depend on specific type systems. This general framework
can have multiple applications to combine the best of both worlds: for
instance, it can be used to add use-site variance annotations to the
Scala type system. We show one such application in detail: we extend
the Java type system with a mechanism that modularly infers the
definition-site variance of type parameters, while allowing use-site
variance annotations on any type-instantiation.

Applying our technique to six Java generic libraries (including the
Java core library) shows that 20-58% (depending on the library) of
generic definitions are inferred to have single-variance; 8-63% of
method signatures can be relaxed through this inference, and up to 91%
of existing wildcard annotations are unnecessary and can be elided.

Parsing Reflective Grammars

Paul Stansifer (Northeastern University)

Existing technology can parse arbitrary context-free grammars, but
only a single, static grammar per input.  In order to support macro
systems that can locally introduce arbitrary new syntax (as opposed to
syntax constrained to S-expressions), we propose reflective grammars,
which can add new rules to their grammars during parsing.  We
demonstrate an algorithm for parsing reflective grammars. The
algorithm is based on Earley's algorithm, and we prove that it
performs asymptotically no worse than Earley's algorithm on ordinary
context-free grammars.

Virtualizing Real-World Objects

Daniel Winograd-Cort (Yale University)

Every programming language has some way of communicating with the
outside world.  Usually we refer to such mechanisms as input/output,
or I/O. In our opinion, conventional I/O mechanisms represent an
awkward disconnect between the internal execution of a program and the
objects, devices, and protocols in the real world. Furthermore, the
I/O interface typically does not distinguish between different kinds
of real-world objects -- everything is treated the same.

In this talk we introduce a radically different approach to
I/O. Instead of treating real- world objects as being external to the
program, we expand the sphere of influence of program execution to
include, indeed subsume, the real world. No longer are "commands" sent
to or received from a device -- instead, the device is a functional
value in the program, just like an arithmetic operator. We call this
approach virtualizing real-world objects.

But the idea runs deeper. Virtual objects (such as GUI widgets) can be
handled in the same way -- and thus we virtualize virtual objects as
well. Furthermore, the approach can be generalized to include
non-local effects, such as is needed for debugging (using something
that we call a wormhole) and random number generation.

Our methodology might seem naive -- for example, how does one prevent
a virtualized device from being copied, thus potentially introducing
non-determinism as one part of a program competes for the same
resource as another? To solve this problem, we introduce the notion of
resource types that assure that a virtualized object is not duplicated
and that I/O and non-local effects are safe. Perhaps just as
important, resource types provide a deeper level of transparency given
for free at the type level; by inspecting the type, one can clearly
see exactly what resources are being used. By using an arrow-based
framework, higher-order types, and type families, we are able to
implement our ideas in Haskell. The result is a safe, effective, and
transparent approach to I/O.

Further Developments in Forlan

Alley Stoughton

Forlan is an open source formal language theory toolset that I've been
developing over the last decade.  It's intended to facilitate
sophisticated experimentation with formal languages, and is embedded
in Standard ML.  In this talk, I will focus on work not reported in my
FDPE '08 paper, "Experimenting with Formal Languages using Forlan".
Some of this work predates the publication of this paper, and some of
it is more recent, or is ongoing.  I will focus on:

 * JForlan, a complete redevelopment of the graphical editor for
   Forlan automata and trees;

 * simplification of regular expressions, finite automata and

 * implementation of additional closure algorithms for finite
   automata and grammars;

 * conversion of finite automata to regular expressions using regular
   expression finite automata; and

 * the functional programming language used as an alternative to
   Turing machines.

I will also talk about future plans for Forlan.


From Java to Lime: Sequential to Parallel, Imperative to Functional, Homogeneous to Heterogeneous

Joshua Auerbach (IBM Research)

Lime is a new language developed in the Liquid Metal project at IBM
Research. Lime targets managed environments with a heterogeneous mix
of CPUs, GPUs, FPGAs, and other accelerators. Lime's strengths include
source and binary level compatibility with Java, and a methodology for
gradual migration from sequential, imperative code to parallel,
functional code that better fits heterogeneous hardware. Lime permits
imperative parts of a program to remain largely unchanged, and allows
the programmer to focus on smaller parts that need modification. Such
changes are designed to be "just enough" to permit the compiler to
infer areas that are functional, parallel, and capable of being
offloaded from the CPU to a GPU or FPGA.

The talk will demonstrate the Lime language, development environment,
compiler, and runtime support, as well as Lime's novel approaches to
both data flow and map/reduce styles of programming. The talk will
also present language support to identify pure functions in a natural
way, that meshes well with an imperative object-oriented language.

See the Web for earlier publications and details of the project.

Asynchronous Assertions

Edward Aftandilian (Tufts University)

Assertions are a powerful bug detection technique. Traditional
assertion checking, however, is performed synchronously, imposing its
full cost on the runtime of the program. As a result, many useful
kinds of checks are impractical because they lead to extreme

We present a solution that decouples assertion evaluation from program
execution: assertions are evaluated asynchronously while the program
continues to execute. Our technique ensures that the assertion
checking thread sees a consistent snapshot of the global state from
the moment the assertion is issued, and that an assertion always
produces the same result as it would in a serial execution. In
addition, asynchronous assertions may be written as though they will
be executed synchronously; no explicit synchronization with the
program is necessary.

We implemented our technique in a system called STROBE, a
snapshot-based system for asynchronous assertion checking in both
single-and multi-threaded Java applications. STROBE runs inside the
Java virtual machine and uses copy-on-write to build snapshots
incrementally. We find that asynchronous checking scales almost
perfectly over synchronous checking in many cases, indicating that the
snapshot overhead is quite low. STROBE provides tolerable overheads
(under 2X) even for heavy-weight assertions that would otherwise
result in crushing slowdowns.

Polymorphic Contracts

Michael Greenberg (University of Pennsylvania

Manifest contracts track precise properties by refining types with
predicates---e.g., {x:Int | x > 0} denotes the positive integers.
Contracts and polymorphism make a natural combination: programmers can
give strong contracts to abstract types, precisely stating pre- and
post-conditions while hiding implementation details---for example, an
abstract type of stacks might specify that the pop operation has input
type {x:'a Stack | not (empty x)}. We formalize this combination by
defining FH, a polymorphic calculus with manifest contracts, and
establishing fundamental properties including type soundness and
relational parametricity. Our development relies on a significant
technical improvement over earlier presentations of contracts: instead
of introducing a denotational model to break a problematic circularity
between typing, subtyping, and evaluation, we develop the metatheory
of contracts in a completely syntactic fashion, omitting subtyping
from the core system and recovering it post facto as a derived

Last modified Monday, February 28th, 2011 6:40:52pm