Lambda, The Ultimate TA, Benjamin C. Pierce, ICFP 2009

Benjamin C. Pierce. Lambda, The Ultimate TA: Using a Proof Assistant to Teach Programming Language Foundations, September 2009. Keynote address at International Conference on Functional Programming (ICFP).

ICFP 2009
video
slides

And related material,

Online book Software Foundations.

Lecture notes Software Foundations (CIS 500), spring 2010 .

Compare with LTU 2008 here