Types and Programming Languages by Pierce is an amazing book. I'm still far from finishing it, but if anyone is looking for a good introduction to the field, this is it. I consider it to be kind of like the SICP of PL. :)

Edit: Ah, and the Software Foundations books are amazing. I did a little course on formal verification during 2020 and learned a ton. Now every time I work with some kind of type system, I feel frustrated that I can't express everything that I want to in my type system.