Yeah, Essentials of Programming Languages is also another great implementation-oriented text, it has some formal things like inductive sets (which pop up in PLT anyway) and also lots of programming exercises.