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 Manolios.
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 Haskell.
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 grammars; * 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 slowdowns. 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
property.
| Last modified Monday, February 28th, 2011 6:40:52pm |