I don't understand exactly what you are looking for, I'll try to explain the Curry-Howard correspondence in a nutshell, you'll let me know if it helps.
The Curry-Howard correspondence (or isomorphism, if you wish) definitely links the three objects you mention: it actually tells that two of them, IL and $\lambda$c, are the same thing. The term is used today in a broad sense and often without referring to a specific technical statement, but it can be formulated precisely in at least two frameworks:
- Hilbert-style deduction for intuitionistic logic and SK combinators;
- Gentzen's natural deduction and the $\lambda$-calculus.
The first is actually the "original" correspondence, dating back to the late 50s when Curry observed that the types you would give to the SK combinators
$$
\begin{align*}
S &:(A\rightarrow B\rightarrow C)\rightarrow(A\rightarrow B)\rightarrow A\rightarrow C \\
K &:A\rightarrow B\rightarrow A
\end{align*}
$$
are exactly the axioms of implicational propositional intuitionistic logic in Hilbert-style deduction. Note that this latter has only modus ponens as a rule for building proofs; accordingly, terms in combinatory logic are built using only application.
That's it for the combinatory logic side. It took another decade before Howard fully formulated the correspondence in the second guise, which I think looks best:
- on the logical side, you have $\mathbf{NJ}^{\Rightarrow,\land}$, Gentzen's natural deduction system for the negative fragment of propositional intuitionistic logic. You have propositional formulas defined by $A,B::=\alpha\mathrel{|} A\Rightarrow B\mathrel{|} A\land B$ (atom, implication and conjunction), proofs built from introduction and elimination rules for each connective, and you have proof normalization, which consists in 2 rewriting rules replacing what Prawitz calls "detours" (an introduction of a connective immediately followed by its elimination) with more explicit pieces of proof. This rewriting procedure closely corresponds to cut-elimination in sequent calculus, also introduced by Gentzen.
- On the computational side, you have the simply-typed $\lambda$-calculus $\Lambda^{\rightarrow,\times}$, with types defined by $T,U::=o\mathrel{|}T\rightarrow U\mathrel{|} T\times U$ (base, function space and pairs), terms built from constructors ($\lambda$ for $\rightarrow$ and pairing for $\times$) and destructors (application for $\rightarrow$ and projections for $\times$), and $\beta$-reduction, which consists of 2 rewriting rules: the usual one and one for handling projections acting on a pair.
The Curry-Howard correspondence, which is the subject of the book you are reading, has three levels:
- formulas = types: just change the notation swapping $\alpha/o$, $\Rightarrow/\rightarrow$ and $\land/\times$;
- proofs = terms: more precisely, introduction rule=constructor, elimination rule=destructor;
- normalization = reduction: this is harder to write inline, but it's obvious once you write the rewriting rules of the two systems side by side. The correspondence is one-to-one, i.e., one step in $\mathbf{NJ}^{\Rightarrow,\land}$ corresponds to exactly one step in $\Lambda^{\rightarrow,\times}$ and vice versa.
At this level, I hesitate to call this an "isomorphism" because it is not entirely clear what structures are being preserved. Here's where category theory may be of help: if you formulate $\mathbf{NJ}^{\Rightarrow,\land}$ and $\Lambda^{\rightarrow,\times}$ as categories (without being too precise: formulas/types as objects and normal proofs/normal terms as morphisms), then they are isomorphic as Cartesian-closed categories (CCC). Indeed, as I defined them, they both are the free CCC on one object ($\alpha$ if you are a logician or $o$ if you are a computer scientist). So, there you go, you now have a third object into the picture and you get what Robert Harper calls the Holy Trinity (logic, programming languages and categories).
Actually, the above categorical view hides a bit what I think is the most important aspect of the Curry-Howard correspondence, which is normalization = reduction. Somewhat annoyingly, this is left out in current alternative terminologies for the correspondence: people say "proofs as programs" or "formulae as types", nobody says "cut-elimination as computation". To properly accommodate the third level, you'd have to climb a bit up on the higher-dimensional ladder and make $\mathbf{NJ}^{\Rightarrow,\land}$ and $\Lambda^{\rightarrow,\times}$ into 2-categories, or even more (things make sense up to dimension 3 at least).
If you're looking for concrete examples, the above framework isn't very rich but already gives you an idea. Take the second-order definition of natural number: $$\mathsf{Nat}(x):=\forall\alpha.(\forall y.\alpha(y)\Rightarrow\alpha(\mathsf{s}y))\Rightarrow\alpha(0)\Rightarrow\alpha(x)$$
($x$ is an integer if it satisfies every property $\alpha$ which is true for $0$ and is true for $y+1$ as soon as it is true for $y$). Now, erase all first-order information and second-order quantification. You get
$$(\alpha\Rightarrow\alpha)\Rightarrow\alpha\Rightarrow\alpha$$
Translated in types, this is
$$\mathsf{N}:=(o\rightarrow o)\rightarrow o\rightarrow o.$$
Guess who are the normal forms of type $\mathsf N$? Exactly the (typed version of the) Church numerals. So every term $\mathsf{N}\rightarrow\mathsf{N}$ is a function on integers. If you keep the first and second order information, you get much more. For instance, the proof in second-order Peano arithmetic that addition is total, i.e., that
$$\vdash\forall x.\forall y.\mathsf{Nat}(x)\land\mathsf{Nat}(y)\Rightarrow\mathsf{Nat}(x+y)$$
gives you a $\lambda$-term of type $\mathsf{N}\times\mathsf{N}\rightarrow\mathsf{N}$. Guess what functions it computes? Well, addition, of course (see Krivine's book "Lambda-calculus: Types and Models"). Cool, isn't it?
Another classical source to learn about Curry-Howard is Girard, Lafont and Taylor's book "Proofs and Types" (but you may already know that, it's in the bibliography of the book you are reading).
