Akkartik: the paper of mine that you cited has a bunch of theorems following the program laid out by Gordon Plotkin in the single best paper I ever read: "Call-by-Name, Call-by-Value and the Lambda Calculus" - a truly profound piece of work that is still worth careful study. But my TOPLAS paper on the topic of LISP can safely be skipped --- the punch-line, as I said, is that the amazing genius John McCarthy messed up the base-case for the definition of his hat(.) function. Stuff happens. In the process, he invented (the very buggy) LISP which was the essential bridge between the true source of sensible computation --- (typed) lambda calculus --- and modern and future software.

(And for what it's worth (ha!) the architect for my present residence was the amazing Terry Heinlein, nephew of Robert Heinlein (of "grok" fame.))