Wanted: a better understanding of constructive logic

I was thinking about how little I understand of type systems today -- I know that they tend to be an embedding of a constructive logic, Int for example, but I don't have any sort of intuitive understanding of what this actually means. This is probably because I haven't done much with intuitionistic logics.

I think that I'll start trying to get a better understanding of intuitionistic logics by reading Eleanor Donovan's honours thesis: "Automated Proof Search in Bi-Intuitionistic Logic Using Sequent Calculi".