This is an observation that the simply-typed lambda calculus and  intuitionistic propositional logic correspond, or in a nutshell:
<ul>
<li>Types are logical formulas.
<li>A term of a type is a proof of that type's formula.
<li>Evaluation corresponds to proof resolution.
</ul>

There are many online documents in postscript on this. <a href= "http://www.cse.psu.edu/~catuscia/teaching/cg520/99Fall/lecture_notes/L11and12.html">Here</a> is one introduction as a plain web page.
