Did he enjoy sections 4 (Metalingustic Abstractions) and 5 (Register Machines)? If so, he'd probably be interested in both these books. They are quite hefty, but seem to be goldmines (so far, I'm only just getting started on them myself). http://research.microsoft.com/en-us/um/people/simonpj/papers... and http://research.microsoft.com/en-us/um/people/simonpj/papers... Both books cover much of the same ground. The fir…
I also enjoyed reading Pierce's Types and Programming Languages (http://www.cis.upenn.edu/~bcpierce/tapl/), although I was kind of nodding my head and going "yeah, whatever" during some of the proofs.