http://lambda-the-ultimate.org/node/2809 Benjamin C. Pierce. Using a Proof Assistant to Teach Programming Language Foundations, or, Lambda, the Ultimate TA . April 2008. White paper. In Fall 2007, I taught an introductory course on logic and the theory of programming languages entirely in Coq. The experience was quite demanding — for the students and especially for me!— but the overall payoff in terms of student engagement and performance on exams far exceeded my hopes. I am now convinced that... read more
