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.
From a CH point of view the logic associated with any Turing-complete language is inconsistent, but this applies to both imperative and functional languages. One could imagine a broadly imperative language without a fully-general "while" construct that could have a useful logical counterpart under CH.
This might be similar to how systems like combinatory logic can in some sense be considered "imperative" languages, since they explicitly act on some kind of logical "state" which works much like state in imperative languages; the only rule of inference being "do A then B then C".