> Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex use

> Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking. See the paper that presented abstract interpretation to the world: "It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..." https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf https://www.di.ens.fr/~cousot/publications.www/CousotCousot-...