Modeling and Reasoning about DOM Events

Benjamin Lerner, Matt Carroll, Dan Kimmel, Hannah Quay-de la Vallee and Shriram Krishnamurthi

The paper (WebApps 2012) (pdf)

The Redex mode (Racket)

The annotated Level 3 Events spec (html)

The github repository here