The answer to your question comes in three parts.
Part one, I think you're mixing up two slightly different uses of 'Type Theory'.
I am guessing Type Theory, as you are used to it, is the field of study where we make type theories, which are formal systems where we add types to terms such that we can combine them together in sensible ways, such that we avoid paradoxes and other nasty things.
The 'Type Theory' that is equivalent to HOL, is more properly called 'Simple Type Theory', which is a kind of type theory (I apologise for the confusing sentence). In essence, 'Simple Type Theory' is just a formal system of terms and types, and is just another name for Higher Order Logic.
Also, I have to be careful here, because Higher Order Logic also has two meanings. The first sense is as a kind of logic. First order logic can quantify over objects from the domain of discourse (the set of all things we want to talk about). For example $\forall x. \forall y. x = y$ is the statement in first order logic that everything in the domain of discourse is equal.
Second order logic can quantify over the set things can be in, third order logic can quantify over the set of sets things can be in, and so on. Higher order logic is then a logic that can quantify over everything $n$-order logic can, for all $n$. Simple Type Theory is just a (but not the only) higher-order logic.
The fact that 'higher order logic' is synonymous with simple type theory came about because, as best I can tell, the HOL proof assistant used a slight extension of the Simple Type Theory as their type theory/logic, and the name stuck.
Part two, on logic and type theory.
The difference between type theory and logic can be somewhat convoluted (I even confused myself in an earlier revision of this answer). This is mainly due to how intertwined they are.
Type theory came about, in part, because of fundamental problems with logic discovered in the early 1900s by Russell and his peers. Summarising Russell's basic idea, the problems he was having was due to self reference, so he added types to proofs such that every proof term lived in a type, and constructed it in a way such that they weren't self-referential.
Part three, the Curry-Howard correspondence.
Type Theory, Logic, and Computation are linked in a rather fundamental way in what is called the Curry-Howard correspondence, which you mentioned. This says that every type theory can be interpreted both as a logic, and also as a computation.
The quintessential example of this is the correspondence between the simply typed lambda calculus and intuitionistic logic.
To explain the notation I'm about to use, think of $\Gamma$ as a multiset which contains assumptions/in-scope variables. $\Gamma, x : A$ is an abbreviation for $\Gamma \cup \{x : A\}$.
$x : A$ means term $x$ has type $A$, and $\Gamma \vdash x : A$ means that 'under the assumptions $\Gamma$, $x$ has type $A$'.
Finally, $\dfrac{J_1 \quad\; J_2 \quad \dots \quad J_n}{J}$ is called an inference rule, and it says, if we have all the things on the top ($J_1,J_2,\dots,J_n$) we can deduce the bottom ($J$).
Here is a fragment of the simply typed lambda calculus:
The first rule is about assumptions, and it says that, if $x : A$ is in our assumptions, then under $\Gamma$, $x$ has type $A$.
$$
\dfrac{x : A \in \Gamma}{\Gamma \vdash x : A}\text{assume}
$$
Rules for lambda terms. Here we have 'abstract', which says if we have an assumption in $\Gamma$, and a construction of a typing $y : A$ we can construct a function from things of type $A$ to things of type $B$.
'apply' says that, if we have a function from $A$s to $B$s, and an $A$, we can get a $B$.
$$
\dfrac{\Gamma, x : A \vdash y : B}{\Gamma \vdash \lambda x. y : A \to B}
\text{abstract}
\qquad
\dfrac{\Gamma \vdash m : A \to B \quad\; \Gamma \vdash n : A}{\Gamma \vdash m \, n : B}\text{apply}
$$
Rules for product. These talk about how to construct and destruct 2-tuples.
$$
\dfrac{\Gamma \vdash x : A \quad\; \Gamma \vdash y : B}{\Gamma \vdash \langle x, y \rangle : A \times B}
\qquad
\dfrac{\Gamma \vdash z : A \times B}{\Gamma \vdash \mathbf{fst}\; z : A}
\qquad
\dfrac{\Gamma \vdash z : A \times B}{\Gamma \vdash \mathbf{snd}\; z : B}
$$
Now, if you ignore everything to the left of the $:$ (that is, ignoring the terms), you get intuitionistic logic (well, specifically, the fragment with only implication and conjunction, but there are analogous constructs for disjunction, truth, and falsity).
If you ignore everything to the right of the $:$ you have the lambda calculus, which is a method of computation.
For more, see Philip Wadler's talk Propositions as Types.