Publications

Modular Proof Development in ACL2, Ph.D. Dissertation. Northeastern University, Boston, MA, 2012. Dissertation (PDF)

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, and Robert Bruce Findler. POPL 2012, Philadelphia, PA. Paper (PDF)

Hygienic Macros for ACL2, Carl Eastlund and Matthias Felleisen. TFP 2010, Norman, OK. Paper (PDF) / Slides (PDF)

Making Induction Manifest in Modular ACL2, Carl Eastlund and Matthias Felleisen. PPDP 2009, Coimbra, Portugal. Paper (PDF) / Slides (PDF)

Sequence Traces for Object-Oriented Executions, Carl Eastlund and Matthias Felleisen. Scheme Workshop 2009, Boston, MA. Paper (PDF) / Slides (PDF)

Automatic Verification for Interactive Graphical Programs, Carl Eastlund and Matthias Felleisen. ACL2 2009, Boston, MA. Paper (PDF) / Slides (PDF)

DoubleCheck Your Theorems, Carl Eastlund. ACL2 2009, Boston, MA. Paper (PDF) / Slides (PDF)

Toward a Practical Module System for ACL2, Carl Eastlund and Matthias Felleisen. PADL 2009, Savannah, GA. Paper (PDF) / Slides (PDF)

Functional Programming and Theorem Proving for Undergraduates: A Progress Report, Rex Page, Carl Eastlund, and Matthias Felleisen. FDPE 2008, Victoria, B.C., Canada. Paper (PDF) / Slides (PDF)

ACL2 for Freshmen: First Experiences, Carl Eastlund, Dale Vaillancourt, and Matthias Felleisen. ACL2 Workshop 2007, Austin, TX. Paper (PDF) / Slides (PDF)

Sequence Traces for Object-Oriented Executions, Carl Eastlund and Matthias Felleisen. Technical report NU-CCIS-06-11, October 2006. PDF

Talks

Hygienic Macros for the ACL2 Theorem Prover, Carl Eastlund and Matthias Felleisen. IFL 2009, South Orange, New Jersey. Slides (PDF)