Publications

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)