[PRL] Torture Chamber on Friday (1pm, WVH 366)

Carl Eastlund cce at ccs.neu.edu
Thu May 13 11:31:07 EDT 2010


Tomorrow (Friday, 5/12) I'll be practicing my talk for TFP in room 366
at 1pm.  The topic is Hygienic Macros for ACL2.  I'm practicing for a
25-minute time slot at the conference.  Here's the abstract for the
paper:

ACL2 is a theorem prover for a purely functional subset of Common
Lisp. It inherits Common Lisp's unhygienic macros, which are used
pervasively to eliminate repeated syntactic patterns. The lack of
hygiene means that macros do not automatically protect the producers
or consumers of macros from accidental variable capture.  This paper
demonstrates how this lack of hygiene interferes with theorem proving.
It then explains how to design and implement a hygienic macro system
for ACL2. An evaluation of the ACL2 code base shows the impact of this
hygienic macro system on existing libraries and practices.

Carl Eastlund



More information about the PRL mailing list