Thought this was quite an interesting paper. It discusses how to specify a Common Lisp-like language very precisely by using the language itself, the way Arc does.
It's also interesting because it shows how few axioms it takes to define large parts of CL, even though CL is hugely complex and was never developed with that intention. It makes me feel confident that Arc will never need a large number of axioms, and that if it looks like it does then someone's doing something wrong.