Lambda the Ultimate

In a G+ request, Norman Ramsey says he wants spice up his PL survey course with a little bit of "cultural enrichment" to show my students the "propositions as types" approach to proof. He's looking for source materials, and, I take it, experiences from people who have tried to teach similar things.