Lectures on the Curry-Howard Isomorphism.

I recently found the following lengthy report on the Curry-Howard isomorphism. 
It was difficult to track down, so I've placed a PDF at:

   http://lambda.ballistichelmet.org/curry-howard.pdf

Morten Heine B. Sorensen, Pawel Urzyczyn:
Lectures on the Curry-Howard Isomorphism.
DIKU report 98/14.

The report contains an introduction to the Curry-Howard Isomorphism
including chapters on untyped and typed lambda-calculi as well as
chapters on formal logics and their semantics, e.g.  Heyting algebras
and Kripke models.