The talk by Steele linked in the OP is very good. I recall attempting to read a PL paper for the first time. My background is in mathematics so I found it a fu

The talk by Steele linked in the OP is very good. I recall attempting to read a PL paper for the first time. My background is in mathematics so I found it a fun puzzle trying to figure out what the notation meant. I think I maybe managed to look up a few things and it was reasonably easy to guess the rest. Some things are very hard to search for (how do you google the notation for inference rules where a horizontal line separates the antecedents from the consequents? I spent 20 minutes trying to find the name for the notation and failed). The other difficulty with reading PL papers is that you need to know that often you should just read the introduction and definitions and skip the extremely long and tedious proofs by structural induction of (somewhat boring) properties like soundness. It tends to be the case that the contents of these proofs is not generally useful (though it is often necessary that such things are proven).