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