I can feel that… and I actually think there are two separate “barriers” (maybe more, I’m speaking of my experience with trying to read PLT papers):
Definitely learn the notation used, there’s Crash Course on Notation in Programming Language Theory which gives a good overview.
Get accustomed in thinking with inductive definitions — Logical Foundation’s chapter Inductively Defined Propositions is very good and also contains exercises in Coq.
🇬🇧 The UK geoblock is lifted, hopefully permanently.
I can feel that… and I actually think there are two separate “barriers” (maybe more, I’m speaking of my experience with trying to read PLT papers):
Definitely learn the notation used, there’s Crash Course on Notation in Programming Language Theory which gives a good overview.
Get accustomed in thinking with inductive definitions — Logical Foundation’s chapter Inductively Defined Propositions is very good and also contains exercises in Coq.