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.

Languages and tools for supporting programmers at design time

Rustan Leino (Microsoft Research)

A programming language is a programmer's primary way to express
software implementations. Mainstream languages today are geared toward
providing the compiler with information that makes its job of emitting
executable code easy. Sometimes, additional information can be useful,
if not to the compiler, to the programmer and to other tools. In this
talk, I will convey a vision for what programming can be like in a
future where language features are geared more toward expressing
designs correctly, where efficiency concerns are addressed separately,
and where tools do more deep semantic analysis while the program is
being developed. During the talk, I will illustrate some of the vision
by demoing tool-supported language features for specifying the intent
of a program (verification), staging the conceptual development of a
program (refinement), and automatically generating code from
data-structure invariants (synthesis).

Programming with People: Integrating Human-Based and Digital Computation

Emery Berger (University of Massachusetts Amherst)

Humans can perform many tasks with ease that remain difficult or
impossible for computers. Crowdsourcing platforms like Amazon's
Mechanical Turk make it possible to harness human-based computational
power on an unprecedented scale. However, their utility as a
general-purpose computational platform remains limited. The lack of
complete automation makes it difficult to orchestrate complex or
interrelated tasks. Scheduling human workers to reduce latency costs
real money, and jobs must be monitored and rescheduled when workers
fail to complete their tasks. Furthermore, it is often difficult to
predict the length of time and payment that should be budgeted for a
given task. Finally, the results of human-based computations are not
necessarily reliable, both because human skills and accuracy vary
widely, and because workers have a financial incentive to minimize
their effort.

This talk presents AutoMan, the first fully automatic crowdprogramming
system. AutoMan integrates human-based computations into a standard
programming language as ordinary function calls, which can be
intermixed freely with traditional functions. This abstraction allows
AutoMan programmers to focus on their programming logic. An AutoMan
program specifies a confidence level for the overall computation and a
budget. The AutoMan runtime system then transparently manages all
details necessary for scheduling, pricing, and quality control.
AutoMan automatically schedules human tasks for each computation until
it achieves the desired confidence level; monitors, reprices, and
restarts human tasks as necessary; and maximizes parallelism across
human workers while staying under budget.

Joint work with Dan Barowy, Charlie Curtsinger, and Andrew McGregor (UMass Amherst). AutoMan and an associated technical report (in submission) are available for download at Web.

A Framework for Verifying Low-level Programs

Gregory Malecha (Harvard University), Adam Chlipala, Patrick Hulin, and Edward Yang (MIT)

High level languages provide abstractions that assist programmers;
however these abstractions are not always sufficient and, in some
cases, they get in the way of writing efficient or functioning correct
code. In this work we develop Bedrock2, a Coq framework for
foundational reasoning about low-level programs using a program logic
based on Ni and Shao's. Bedrock2 is an extension and rewrite of
Chlipala's Bedrock language.

Bedrock2 allows programmers to define both control and data
abstractions and integrate them into the system in a first-class
way. Control abstractions, e.g. conditionals and function calls, are
defined by providing a denotation into the core language and derived
inference rules are verified in a foundational way with respect to the
core language semantics. These inference rules are used by the
verification condition generator simplify the proof obligations
provided to the programmer. Verification conditions are expressed as
pre- and post-conditions on execution traces allowing the bulk of the
work to be done by symbolic evaluation. Unlike Bedrock, the Bedrock2
symbolic evaluator incorporates user-defined abstract predicates to
enable efficient manipulation of arrays, structures, stack frames, and
other data abstractions. Final verification conditions are discharged
using a cancellation-based separation logic prover. Proofs are
generated using computational reflection to enable good performance
that, experiences suggest, will scale to larger programs than previous
work. Bedrock2 embraces a more realistic machine model that exposes
machine word sizes, byte ordering, and finite memory. We are working
to extend the language to more interesting abstractions, real assembly
languages, and concurrency.

Precise Enforcement of Progress-Sensitive Security

Scott Moore, Aslan Askarov, and Stephen Chong (Harvard University)

Program progress (or termination) is a covert channel that may leak
sensitive information. To control information leakage on this channel,
semantic definitions of security should be _progress sensitive_ and
enforcement mechanisms should restrict the channel's
capacity. However, state-of-the-art language-based information-flow
mechanisms are progress insensitive -- allowing arbitrary information
leakage through this channel -- and current progresssensitive
enforcement techniques are overly restrictive.

We propose a type system and instrumented semantics that together
precisely enforce progress-sensitive security. Our system is
permissive in that it is able to accept programs in which the
termination behavior depends only on low-security information (and are
thus secure). We extend the system to permit controlled leakage
through the progress channel, with the leakage bound by an explicit
budget.

Reagents: expressing and composing fine-grained concurrency

Aaron Turon (Northeastern University)

Achieving parallelism is all about eliminating communication costs.
The past two decades have produced a sizable collection of algorithms
for low-cost, fine-grained communication; they lie at the the heart of
industrialstrength libraries like java.util.concurrent.  But while
concurrency libraries are indispensable, they are an enormous
undertaking, and they generally provide a set of primitives that users
cannot easily extend or compose.

In this talk, I will present an approach to building concurrency
libraries based on reagents, a new abstraction for finegrained
communication.  With reagents, algorithms no longer need to be
constructed from "whole cloth" by using system-level primitives
directly. Instead, they can be built incrementally, by composing
abstract primitives. Common patterns can be baked into the primitives
or captured in new abstractions built from them.  Library writers
benefit, because they can express algorithms at a higher level, with
more reuse, *without* sacrificing scalability. Library users benefit,
because composition empowers them to extend and tailor the library
without knowing the details of its underlying algorithms.

ParaSail: A Simplified Approach to Parallel Programming

S. Tucker Taft (AdaCore)

ParaSail (for "Parallel Specification and Implementation Language") is
a language that marries a pervasively parallel computation model with
formal methods. ParaSail achieves most of its power by *removing*
features from the language that act as impediments to parallelization
and formal analysis.  Nevertheless, the language remains very
flexible, and preserves a familiar syntax and generic/objectoriented
programming model similar to that of Java, C#, and C++, using
(generic) interfaces and classes.

Problems of First-Class Functions over Space-Time

Jacob Beal (BBN Technologies)

Aggregate-level abstractions are a useful tool for programming
distributed systems: with an appropriate choice of abstractions, many
of the details of networking, fault recovery, and dynamic scaling can
be made implicit.  The necessity of being able to simultaneously view
a system in terms of aggregate computations and the local computations
that implement them, however, leads to problems in the definition of
distributed function calls, since a distributed function-call may
originate in many locations simultaneously.

I will discuss these problems in the context of Proto, a LISP-like
space-time programming language that abstracts a network of devices as
an approximation of a continuous manifold.  In particular, I will
discuss progress on the following challenges that must be overcome in
order to have first-class functions over aggregates: recursion,
higher-order functions, closures, runtime function definition, and
function equality.

Modeling and Reasoning about DOM Events

Benjamin S. Lerner, Matthew J. Carroll, Dan P. Kimmel, Hannah Quay-de la Vallee and Shriram Krishnamurthi (Brown University)

Web applications are fundamentally reactive. Code in a web page runs
in reaction to events, which are triggered either by external stimuli
or by other events. The DOM, which specifies these behaviors, is
therefore central to the behavior of web applications. We define the
first formal model of event behavior in the DOM, with high fidelity to
the DOM specification. Our model is concise and executable, and can
therefore be used for testing and verification. We have applied it in
several settings: to establish some intended metaproperties of the
DOM, as an oracle for testing the behavior of browsers (where it found
real errors), to demonstrate unwanted interactions between extensions
and validate corrections to them, and to examine the impact of a web
sandbox. The model composes easily with models of other web
components, as a step toward full formal modeling of the web.

The semantics and related materials can be found on the Web.

Blocks Languages for Creating Tangible Artifacts

Franklyn Turbak (Wellesley College)

Logo turtles and Peter Henderson's picture language have long been
used to teach computational thinking in contexts where learners are
inspired to construct programs that create complex geometric
designs. We have developed TurtleBlocks and PictureBlocks, visual
blocks-based versions of these languages whose outputs are tangible
artifacts produced by laser and vinyl cutters. Our languages embody
two novel features. First, they use constructive area geometry to
convert the geometric designs generated by our programs into formats
suitable for laser and vinyl cutters. Second, they leverage static
typing and polymorphism to handle variable references more sensibly
than in other blocks languages.

This talk describes work done with Wellesley College undergraduate students Karishma Chadha, Erin Davis, Emily Erdman, Olivia Kotsopoulos, Johanna Okerlund, and Smaranda Sandu.

Representing Expressive Types in Blocks Programming Languages

Marie Vasek (Wellesley College)

In blocks programming languages, such as Scratch and App Inventor,
programs are created by connecting visual program fragments shaped
like jigsaw puzzle pieces. The shapes of these blocks help novices
avoid frustrating syntax errors commonly encountered in textual
programming languages by strongly suggesting how expressions and
statements are composed to form programs. The shapes of the block
connectors can be used to indicate type, but they currently handle
only base types and do so in an ad hoc and confusing fashion.

The goal of this project is to create a blocks version of a language
similar to ML. Towards this goal, I developed TypeBlocks, which
extends the blocks framework ScriptBlocks with arbitrary compositions
of list, tuple, and function type constructors represented by unique
connector shapes. TypeBlocks also can express polymorphism via special
connectors that change shape according to the context in which they
are used. This project aims to help programmers better understand the
types used in functional programming languages.

Last modified Sunday, May 6th, 2012 3:27:11am