[PRL] Torture Chamber: 9am tomorrow, Hygienic Macros for the ACL2 Theorem Prover

[Carl Eastlund]

Oh yeah, and the extended abstract (copy/pasted from the PDF):

ACL2 is the successor of the Nqthm theorem prover, Boyer and Moore’s
first attempt to build an automatic theorem prover for a theory of first-order
functional programming [1]. Its development began in the 1980s in response
to efficiency and expressivity problems with Nqthm [2]. ACL2 combines the
applicative subset of Common Lisp with a first-order theorem prover over a
logic of total functions. The system has been used to model and verify large
commercial hardware and software artifacts.

In addition to the functional language, ACL2 also inherits the macro system
from Common Lisp. Roughly speaking, the macro system is a mechanism for
extending the notation of the language via functions that operate on syntax
trees. According to Kaufmann and Moore [2], “one can make specifications more
succinct and easy to grasp . . . by introducing wel l-designed
application-specific
notation .” Indeed, macros are used extensively in ACL2 libraries.

Unfortunately, Common Lisp macros are unhygienic [3], meaning a macro’s
variable bindings may accidentally shadow program variables or vice
versa. These
accidental captures not only violate a programmer’s intuition of
lexical scope but
also break logical reasoning about the program source.

Over the last 20 years, the Scheme community has produced hygienic macro
systems that keep bindings inside macros separate from those outside [3, 4].
These hygienic systems avoid the pitfalls of Lisp macros, as macro writers need
not document all the variables they bind internally and macro users need not
avoid duplicating them.

In this talk, we present the proof-technical motivation, the design, and the
implementation of a hygienic macro system for ACL2. We adapt the data repre-
sentation and expansion algorithm of Dybvig et. al. [5] to support
Lisp’s separate
function and value namespaces as well as ACL2’s “encapsulation” mechanism.

On Mon, Sep 21, 2009 at 12:30 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> Room change: we will be in 366.
>
> On Mon, Sep 21, 2009 at 12:24 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
>> I will be practicing my IFL talk tomorrow morning at 9am in room 164.
>> The talk has a 25 minute slot, so I will speak for about 20 minutes
>> and then you can all get out the thumbscrews.
>>
>> Carl Eastlund