TTOP is the standard work on the topic. Some parts I would say fell out of fashion (using Miranda for example), but many parts are either timeless or still just as relevant.

That said, the book is very dense; for me it was just too much the first time I tried to read it. After circling back to it after a while it gets much easier, because you know what parts you really need (which is a common pattern for me at least with everything academic).

Miranda should still be readable for those with some Haskell background (it was a major influence on developing the Haskell language). I also have a more modern update to Miranda called Admiran: https://github.com/taolson/Admiran

TTOP? Do you mean TTFP?

TAPL, I meant TAPL (Types and Programming languages by Pierce)! This would not have happened with a well-typed comment section. I mixed up OP's book (which is nice as well!) and the abbreviation. Sorry!

Sure, why not. It seems to be a pretty good exposition of the material. When I got interested in this stuff many years ago I worked my way through the 'typing rules' in the coq (nowadays rocq) manual. That is a 'slightly' higher friction way of learning this stuff. This document seems to be more pedagogical.

Have you found this stuff useful during the many years since you learned it? Or you don't mean you mastered it enough to judge its usefulness?

I have a personal coq/rocq project regarding the verification of software so for that purpose it is highly useful. I also wrote a proof assistent myself (https://github.com/chrisd1977/system).

A related book (seems to be more often cited) is Types and Programming Languages by Benjamin C. Pierce. That seems to be more concrete (as opposed to theoretical), with chapter titles like "An ML Implementation of {some concept}".

They are very different books. TAPL is a book about programming language semantics, TTAFP is a programmer-oriented book about Martin-Löf type theory.

There is very little overlap.

TAPL is definitely the book to pick up if you are interested in programming language semantics. But if you are interested in logic, dependent types, Curry-Howard correspondence there are potentially better and more modern materials than TTAFP (not to say that TTAFP is bad). If you care about formalizing programs Sofware Foundations is a much better resource, and if you care about mathematics and logic, there are resources specifically suited to that.

What other books would you suggest? I've been reading TTAFP for a few months now and I don't like it very much. I was thinking maybe starting to read Principles of Dependent Type Theory by Angiuli and Gratzer but I'm not sure if it really covers the same area.

TAPL is a perfectly good book, but some in academia will tell you that it is somewhat dated.