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

Carl Eastlund cce at ccs.neu.edu
Thu May 13 11:49:30 EDT 2010


Sorry, we'll be starting at 1:30pm, a half hour later, so as not to
conflict with the final session of HOPL.

Carl Eastlund

On Thu, May 13, 2010 at 11:31 AM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> 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