[logo suggestions welcome]

N
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.


Last modified Sunday, September 30th, 2007 2:01:08pmPowered by PLT