[Pl-seminar] PL seminar schedule

[Aaron Turon]

NEU Programming Languages Seminar presents

Two POPL practice talks:

Christos Dimoulas
Northeastern University

Aaron Turon
Northeastern University

Wednesday, 1/19

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Each talk will run for ~25 minutes, followed by ~45 minutes of
questions and feedback.

**

Correct Blame for Contracts: No More Scapegoating

Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, Matthias Felleisen

Behavioral software contracts supplement interface
information with logical assertions.  A rigorous enforcement of contracts
provides useful feedback to developers if it signals contract violations
as soon as they occur and if it assigns blame to violators with precise
explanations. Correct blame assignment gets programmers started with the
debugging process and can significantly decrease the time needed to
discover and fix bugs.

Sadly the literature on contracts lacks a framework for making statements
about the correctness of blame assignment and for validating such
statements. This paper fills the gap and uses the framework to
demonstrate how one of the proposed semantics for higher-order contracts
satisfies this criteria and another semantics occasionally assigns blame
to the wrong module.

Concretely, the paper applies the framework to the {\em lax\/}
enforcement of dependent higher-order contracts and the {\em picky\/}
one. A higher-order dependent contract specifies constraints for the
domain and range of higher-order functions and also relates arguments and
Abstract

results in auxiliary assertions. The picky semantics ensures that the use
of arguments in the auxiliary assertion satisfies the domain contracts and
the lax one does not. While the picky semantics discovers more contract
violations than the lax one, it occasionally blames the wrong module.
Hence the paper also introduces a third semantics, dubbed {\em indy\/},
which fixes the problems of the picky semantics without giving up its
advantages.

**

A separation logic for refining concurrent objects

Aaron Turon, Mitchell Wand

Fine-grained concurrent data structures are crucial for gaining
performance from multiprocessing, but their design is a subtle art.
Recent literature has made large strides in verifying these data
structures, using either atomicity refinement or separation logic with
rely-guarantee reasoning. In this paper we show how the ownership
discipline of separation logic can be used to enable atomicity
refinement, and we develop a new rely-guarantee method that is
localized to the definition of a data structure. The result is a
comprehensive and tidy account of concurrent data refinement that
clarifies and consolidates the existing approaches.