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|