I teach programming languages semantics in two consecutive units, at the university of Nice (first year and second year of the Master in Computer Science program), functional programming and proofs, at the Ecole normale supérieure de Lyon (first year of the Master in Computer Science program), and proof mechanization at the University of Marseilles (second year of the Master entitled "foundations of computer science and discrete mathematics"). In the past, I also taught introduction to formal methods to the university of Marseilles (second year of a master in Computer Science and Statistics).
I taught this course for 5 or 6 years now, the course notes for the consecutive years are listed here (in French).
This course is more recent and revolves more around the notion of proofs about programming language semantics. The course notes are listed in this page.
I also taught a course of introduction to Coq at various levels. The most intensive was at Ecole Normale supérieure, but everything was with chalk on the blackboard, so there is no electronic data to show for it. The material I used was mostly fragments of our book on Coq, but more details are given in this page.
I also taught an introductory course on Coq at Tsinghua University in China in April 2008. Here is a link to the documents I prepared for this event.
At the end of August 2009, INRIA and Tsinghua University in Beijing organize a summer school on Coq, where I will present some introductory material