All recent courses can also be found on
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