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