Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming

• Coq soundness proof and OCaml implementation (supporting our CSF 2013 submission): slamjs-2013-02-13.tar.gz
• From LOng Lunch Seminar (verification audience): original slides or with proof sketch.
• From OXFORD-CS-2012 internal student conference (general computer science audience): abstract, poster and slides.

More material, including an updated version of the CSF supporting materials, and some relating to our PLAS 2013 paper, will appear in the next couple of weeks! -- 2013-06-27