[PRL] Fwd: Talk Announcement: David Van Horn (Northeastern), July 7, 1:30pm, Room TBA

[David Van Horn]

Below is an announcement for a talk I'm giving across the river next 
Wednesday.  Many of you may have seen the first half of what I'll be 
talking about at the most recent NEPLS.  The second half is recent work 
with Matt Might and Christopher Earl and is very related to Dimitris and 
Olin's work on CFA2 (ESOP 2010).

Also, Chris Skalka, my MS adviser, will be around (at Harvard) on 
Wednesday and Thursday.  Let me know if you want me to set something up 
with him.  I think PRL members might be interested in his latest 
Staged-ML work and also his work on types and separation logic.  For 
details, see:

    http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-pubs.html

David

-------- Original Message --------
Subject: Talk Announcement:  David Van Horn (Northeastern), July 7, 
1:30pm, Room TBA
Date: Wed, 30 Jun 2010 17:08:16 -0400
From: Jeff Vaughan <jeff at seas.harvard.edu>
To: programming at eecs.harvard.edu, CRCS affiliates 
<crcs at eon.law.harvard.edu>,        slap at eecs.harvard.edu, Greg Morrisett 
<greg at eecs.harvard.edu>,        Stephen Chong <chong at seas.harvard.edu>, 
        Matthieu Sozeau <mattam at mattam.org>, Adam Chlipala 
<adam at chlipala.net>,        Jean-Baptiste Tristan 
<jean.baptiste.tristan at gmail.com>,        Jeff Vaughan 
<vaughan2 at seas.upenn.edu>,        David Van Horn <dvanhorn at ccs.neu.edu>

Talk Announcement:

David Van Horn (Northeastern)
July 7, 1:30pm, Room TBA

Abstracting Abstract Machines: Storing and Stacking Continuations

We describe two techniques for systematically deriving abstract
interpretations approximating canonical machines for higher-order
languages.  The first allocates continuations in a bounded store to
achieve a finite state-space.  We demonstrate the generality of this
approach by transforming the CEK machine of Felleisen and Friedman, a
lazy variant of Krivine's machine, and the stack-inspecting CM machine
of Clements and Felleisen into abstract interpreters.  The technique
scales up uniformly to allow static analysis of realistic languages
features, including tail calls, conditionals, side effects,
exceptions, first-class continuations and even garbage collection.

The second technique keeps continuations on the stack to achieve a
push-down model of abstract interpretation.  The resulting abstract
interpreter always matches calls and returns, achieving a higher level
of precision by never conflating call and return pairs.  Although this
technique produces abstract interpreters with infinite state-spaces, we
demonstrate how basic static analysis questions remain decidable by
casting them as language inclusion problems answered by push-down automata.

(Joint work with Matthew Might and Christopher Earl, University of Utah)

David Van Horn is a CRA Computing Innovation Fellow working at
Northeastern University's Programming Research Lab. He received his PhD
from Brandeis University in 2009.