# Is there a correspondence between the syntaxes and the type systems of programming languages?

I was reading the first chapter of Robert Harper's Practical Foundations for Programming Languages in which it introduced abstract binding trees, aka abt. It seems pretty like typed lambda calculus.

1. There are ground sorts, which are similar to ground types in typed lambda calculus.
2. There are abstractions; they accept multiple arguments. They remind me of uncurried version of lambdas. It's a bit odd that abstractions at the syntax level aren't first-class, though.
3. Later at the end of the chapter in the book, symbols are introduced. They seem to correspond to data types. (Or do they?)
4. Indexed operators are $\Lambda$ bounded terms in the sense of system F.

The author of the book seemed to be aware of the similarities. The set of symbols is even written $\mathcal{U}$ in the book!

What I'm asking is, is there known to be a correspondence of abt's and type systems, or is it too good to be true? Are there more advanced systems of abt's that correspond to system Fω or dependent types?

The question is kind of too broad. Hopefully it can be accepted on this website.