Lambda the Ultimate

I was wondering if anyone could recommend some good books on the more theoretical aspects of type theory as it pertains to computer science and guarantees w.r.t to certain properties as related to language theory. The only books I know of are the two by Pierce but they seem more on the applied side focusing on very specific applications of various theories that in many cases have a long history which aren't really covered by either book. Are there better books covering some of the theory more in depth?

Thanks.