Functional programming and theorem proving for undergraduates: a progress report. - Rex L. Page; Carl Eastlund; Matthias Felleisen (FDPE@ICFP, 2008)

Toward a Practical Module System for ACL2. - Carl Eastlund; Matthias Felleisen (PADL, 2009)

Making induction manifest in modular ACL2. - Carl Eastlund; Matthias Felleisen (PPDP, 2009)

Hygienic Macros for ACL2. - Carl Eastlund; Matthias Felleisen (Trends in Functional Programming, 2010)

Run your research: on the effectiveness of lightweight mechanization. - Casey Klein; John Clements; Christos Dimoulas; Carl Eastlund; Matthias Felleisen; Matthew Flatt; Jay A. McCarthy; Jon Rafkind; Sam Tobin-Hochstadt; Robert Bruce Findler (POPL, 2012)