All recent courses can also be found on this page or this page.

Yves Bertot's teaching activities

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).

Cours de Coq : 8-hour video introductory course on Coq (in French)

This course contains small videos (ten minutes on average) with explanations in French. It also contains a few demonstrations performed "live" on the computer. This course is available at the following address, the source of the slides are available from the following page.

Computer Assisted Proofs

This course for first year master's students is taught for the first time during the fall term of 2012. Courses notes should be available from the following page.

A new version is organized as a one-week intensive course, which already happened in 2014 and in 2015. The page for 2014 is here, The page for 2015 is here. These courses are usually attended by students from many universities in France.

Programming languages semantics (1)

I taught this course between 2001 and 2012, the course notes for the consecutive years are listed here (in French).

Programming language semantics (2)

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.

Functional programming and Proofs

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.

An introduction to Coq

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.


Yves Bertot
Last modified: Fri Apr 15 15:14:12 MEST 2005