Proofs are Programs
Lately I've been asked to name a paper that could serve as an introduction to type systems and program proofs. I mentioned Proofs are Programs: 19th Century Logic and 21st Century Computing by Philip Wadler (he gave a similar paper at ILC03 in New York). To my delight Wadler's paper was mentioned at Lambda the Ultimate in a list of Natural Deduction Reading for Beginners .
BTW lispmeister.com has been offline for a couple of days due to a denial of service attack. Seems like that's the kind of risk you have to take, if you do botnet research.