![[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.
BAT: The Bit-level Analysis Tool
Pete Manolios (Northeastern University)
The Bit-level Analysis Tool (BAT) is a system for verifying bit-level problems arising from hardware, software, and security domains. BAT implements a state-of-the-art decision procedure for solving quantifier-free formulas over the extensional theory of fixed-size bit-vectors and fixed-size bit-vector arrays (memories). Our primary goal in developing BAT is to enable the verification of system-level properties of systems described at the bit-level; an example is the verification of bit-level pipelined machine models. Key features of the BAT system are an expressive strongly-typed modeling and specification language, a fully automatic and efficient memory abstraction algorithm for extensional arrays, and a novel CNF generation algorithm. The BAT system can be used to automatically solve system-level RTL (Register Transfer Level) verification problems that were previously intractable, such as refinement-based verification of RTL-level pipelined machines.
Session Types Made Boring
Alec Heller and Riccardo Pucella (Northeastern University)
Session Types are a technology for ensuring that concurrent processes adhere to specific protocols. By giving a channel a type that describes what data may be sent over it at which points in the code, we may reject programs with incorrect communication behavior at compile time. For example, we might have an arithmetic server, which accepts the arguments to some operation from a client thread and then sends back the result of the computation. In a language such as Concurrent ML, the type of the channel would describe only that data sent over the channel are integers. It would have no information about which party was responsible for sending which information in what order. Thus code which participated in such a protocol would need to manage the protocol at every step. In a language with Session Types, we could say that the type of the channel for doing arithmetic was "Send an Int, Send an Int, Receive an Int". We present a simple type system for Session Types in a concurrent, functional language such as Concurrent ML. Our approach makes Session Types easier to reason about and integrate into programming languages than previous treatments of the subject. We make Session Types "boring" by re-expressing them using well understood, standard programming language technology (linear lambda calculus, capabilities, etc.) instead of the previous more ad hoc presentations.
vau-calculi and the theory of fexprs
John N. Shutt (WPI)
Fexprs are an ancient Lisp technology alternative to macros. Like macros, they can act on their unevaluated operands, but like Scheme procedures, they are first-class objects. Fexprs have been deprecated since about 1980 due to ill-behavedness concerns. Use of fexprs in a program may cause other language features ---such as the Lisp lambda operator--- to behave in unexpected ways. A theoretical consequence of this behavior is that if the lambda operator of lambda-calculus is required to mathematically model the lambda operator of Lisp, the behavior of calculus lambda must be altered when introducing fexprs, causing meltdown of the well-behavedness properties of lambda-calculus. Mitchell Wand explored this effect in detail in a 1998 paper, "The Theory of Fexprs is Trivial". This talk describes a novel calculus, called vau-calculus, that supports a different mathematical model of fexprs than that studied by Wand. Rather than represent Lisp lambda directly by calculus lambda, vau-calculus models execution of a Lisp program by explicit evaluation of a passive data structure. Lambda-calculus is embedded in vau-calculus, and assists in the explicit evaluation process. By relaxing the correspondence between Lisp lambda and calculus lambda, vau-calculus reconciles fexprs with nontrivial semantic theory. Thus, one can have any two, but not all, of these three elements: nontrivial theory, fexprs, and perfect Lisp lambda/calculus lambda correspondence. The usual approach to Lisp semantics omits fexprs. The approach studied by Wand lacks a nontrivial theory. The vau-calculus approach lacks the perfect correspondence; but because it has the other two elements, it can be used to study how the correspondence breaks down ---and when it doesn't--- in the presence of fexprs.
Relationally-Parametric Polymorphic Contracts
Arjun Guha (Brown University)
The analogy between types and contracts raises the question of how many features of static type systems can be expressed as dynamic contracts. An important feature of types missing in prior work on contracts is relational parametricity, as represented by the polymorphic types in languages like Standard ML. We'll explore an interpretation of such types as enforceable run-time contracts.
Joint with work with Jacob Matthews, Robby Findler, and Shriram Krishnamurthi. Details are in our DLS 2007 paper.
Functional programming in the wild: Sensor Networks, Streams, and
Parallelism
Ryan Newton (MIT), Greg Morrisett (Harvard) and Sam Madden (MIT)
We present WaveScript, a domain-specific language for processing live data-streams in embedded, parallel, and distributed contexts. I will discuss a recent sensor network deployment in which we used WaveScript to acoustically localize marmots (medium sized mammals) in Colorado, using a distributed microphone array. WaveScript is an ML-like language with built-in constructs for stream processing. A WaveScript program executes over a multi-tiered network of sensors, with a single application spanning hardware platforms from embedded devices to multicore, multiprocessor servers. WaveScript uses a two-stage evaluation model (metaprogramming) to enable highly abstract, polymorphic, and modular stream programs without loss of performance. In fact, the programs produced by the compiler are first-order, monomorphic dataflow graphs. Abstracting the construction of these dataflow graphs enables both reusable libraries as well as the prospect of building new stream abstractions by changing the glue used to compose stream-graphs.
