[PRL] PL seminar schedule

[Aaron Turon]

I need a bit more time to prepare and practice my talk, so tomorrow we
will just have a torture chamber for Christos.

On Tue, Jan 18, 2011 at 9:17 AM, Aaron Turon <turon at ccs.neu.edu> wrote:
> 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.
>