Another introduction, with emphasis on the historical development:
Philip Wadler, "Proofs are Programs: 19th Century Logic and 21st
Century Computing."
http://www.cs.bell-labs.com/who/wadler/topics/history.html
It's a fun read, too.
Cheers,
Tom