Is there any sort of formal definition of terms like 'data type', 'abstract data type', etc?

Question

If not (because I assume not) is there some kind of reference or book that provides some theoretical foundation to these concepts? I've been learning about data structures and abstract data types for a while now but all these concepts seem very hazy and I would like some sort of rigorous grounding to stand on.

I hear type theory is used to found a lot of theoretical computer science (or all of it). So where could I read about type theory and how it is used to formalize CS?

Answer 1

I good starting point is Benjamin Pierce's Types and programming languages (popularly referred to as "TAPL").