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.
Implementing Data Race Detection
Benjamin Wood (Wellesley College)
Researchers have proposed data-race exceptions for clear semantics and improved debugging support in shared-memory multithreaded programming languages. Implementing accurate and fast support for data-race exceptions remains a challenge. This talk considers a small family of problems and opportunities in language implementation and dynamic program analysis arising from experience designing a fully accurate hardware-supported dynamic data-race detector. For example: How can a low-level (e.g., ISA-level) dynamic program analysis effectively analyze programs in higher-level programming languages? Can hardware support for accurate data-race detection be generalized to support other analyses? Can software implementations of dynamic analyses emulate performance optimizations that are successful in hardware implementations? This talk describes a mix of completed and ongoing work undertaken with colleagues at the University of Washington, Microsoft Research, and The Ohio State University.
A Core Quantitative Coeffect Calculus
Marco Gaboardi (University of Dundee)
Monadic notions of computation are well-established mechanisms to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this talk, I will present a language inspired by a generalized interpretation of linear type systems. In this language linear types are indexed by a label-an element of a semiring-that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis. I will also discuss an ongoing work about a quantitative calculus combining comonadic coeffects with monadic effects. I will show how a dependency between coeffects and effects corresponds to a distributivity law of (labeled) monads over (labeled) comonads. This dependency can be used to describe context-dependent effect systems.
Will Clinger (Northeastern University)
The R7RS (small) standard for Scheme was approved in 2013. There are now at least eight implementations of R7RS, with more in progress. At least two of the eight implement the previous R6RS standard as well, demonstrating near-perfect backward compatibility with R6RS libraries and programs. An R7RS (large) standard is being developed and is expected to specify libraries that go well beyond those specified by the R6RS.
Design of a Debugger for Memory Managers
Karl Cronburg (Tufts University)
The design and implementation of debuggers targeted at memory managers is crucial given the ever-growing popularity of memory safe systems. Year after year, new managed systems are created and existing ones are constantly developed. This pattern results in an ever-growing need for debugging tools targeted at these systems. In this talk we will discuss the design of a memory management debugger capable of verifying memory layout semantics. Our design uses a system of memory permissions to model the memory management stack. In this design we assign read / write permissions to regions of memory. Permissions are based on where in the memory management stack the region is and what code is running. The key idea is to declaratively specify the layout and ownership of memory, and check that associated invariants are maintained. Our discussion will touch on the implementation of such a debugger for the Jikes RVM Java Virtual Machine. This implementation leverages the Valgrind dynamic binary instrumentation framework and Jikes RVM specific knowledge to verify the read / write permissions of every load / store / modify machine instruction of the JVM execution.
Datatype Derivatives are the Defunctionalization of Continuation-Passing Style
Conor McBride observed in a series of papers that the derivative of a data type describes the single-hole contexts of that type -- that is, to the context half of Huet's zippers. This raises an intriguing question: Is there a connection between the a zipper for a data type and arbitrary functions that traverse that type? It turns out there is: If we perform a local transformation to continuation-passing style and defunctionalize the result, we obtain a family of context types that describe the way the function traverses the data type. These context types are generalized nicely by McBride's "Clowns to the Left of Me, Jokers to the Right". Defunctionalization of CPS reifies the stack of the running program and as a result systematically transforms recursion into iteration (tail recursion). It also provides insight into what we mean when we say that "A Zipper is an iterator for a pure data structure".
Deep Specifications and Certified Abstraction Layers
Ronghui Gu (Yale Univeristy)
Modern computer systems consist of a multitude of abstraction layers (e.g., OS kernels, hypervisors, device drivers, network protocols), each of which defines an interface that hides the implementation details of a particular set of functionality. Client programs built on top of each layer can be understood solely based on the interface, independent of the layer implementation. Despite their obvious importance, abstraction layers have mostly been treated as a system concept; they have almost never been formally specified or verified. This makes it difficult to establish strong correctness properties, and to scale program verification across multiple layers. In this talk, I will present a novel language-based account of abstraction layers and show that they correspond to a strong form of abstraction over a particularly rich class of specifications which we call deep specifications. Just as data abstraction in typed functional languages leads to the important representation independence property, abstraction over deep specification is characterized by an important implementation independence property: any two implementations of the same deep specification must have contextually equivalent behaviors. We present a new layer calculus showing how to formally specify, program, verify, and compose abstraction layers. We show how to instantiate the layer calculus in realistic programming languages such as C and assembly, and how to adapt the CompCert verified compiler to compile certified C layers such that they can be linked with assembly layers. Using these new languages and tools, we have successfully developed multiple certified OS kernels in the Coq proof assistant, the most realistic of which consists of 37 abstraction layers, took less than one person year to develop, and can boot a version of Linux as a guest.
Prioritized GC: Using the Garbage Collector to Support Caching
Diogenes Nunez (Tufts University)
Integrating SMT into Software Development
William Blair (Boston University)
SMT solvers are powerful tools that determine the satisfiability of formulas from different first order theories. These theories are relevant to software verification, yet SMT solvers are considered low level tools that programmers are unlikely to encounter. While languages may support verification features by using SMT solvers, they are unlikely to expose an interface to the solver for the programmer to use. In this talk, we will describe how dependent types in ATS, a statically typed functional programming language, can be a platform for integrating SMT solvers into the software development process. In this process, program types are refined to include static indices (classified by sorts) which model properties of types. Typechecking a program that uses such types automatically generates constraints which must be checked for validity in order for the program to be well typed. In this talk, we describe how exporting constraints to SMT solvers allows a programmer to take advantage of domains understood by SMT solvers in program invariants. We will demonstrate a current prototype of this system that uses Z3 to verify low level programs that utilize fixed width bit vectors and discuss a more generic design that could accomodate more powerful theorem provers in the future.
Implementing a Stepper using Delimited Continuations
Youyou Cong (Ochanomizu University)
In this talk, I present an implementation of a stepper for a subset of OCaml by manipulating delimited continuations. Our stepper receives a program and returns a list of all the elements in the reduction sequence. To construct each intermediate program, we capture the context surrounding the redex that is being focused. In our implementation, the context is obtained using the control operators shift and reset. Our stepper is implemented by writing an interpreter that is close to a typical big-step interpreter. The difference is that it reconstructs the current evaluation context in the cases where the interpreter returns a non-value expression. When a redex is found, the context is captured by the shift operator and is used to reconstruct the current program. This is joint work with Kenichi Asai (Ochanomizu University).
Tracking the Flow of Ideas in the Programming Languages Literature
Michael Greenberg (Pomona College)
How have conferences like ICFP, OOPSLA, PLDI, and POPL evolved over the last 20 years? Did generalizing the Call for Papers for OOPSLA in 2007 or changing the name of the umbrella conference to SPLASH in 2010 have any effect on the kinds of papers published there? How do POPL and PLDI papers compare, topic-wise? Is there related work that I am missing? Have the ideas in O'Hearn's classic paper on separation logic shifted the kinds of papers that appear in POPL? Does a proposed program committee cover the range of submissions expected for the conference? If we had better tools for analyzing the programming language literature, we might be able to answer these questions and others like them in a data-driven way. In this talk, we present some early results showing how topic modeling, a branch of machine learning, might help the programming language community better understand our literature.
|Last modified Thursday, June 4th, 2015 9:37:04am|