I love “Types and Programming Languages” by Benjamin Pierce and always recommend it for people who want to dip their toes into formal type theory. To me it’s basically the K&R for type theory.