In 2000, I gave a tutorial on Coq at TPHOLs2000.

In the past, I taught Coq (in French) to 5th year university students in Nice and Marseilles.

I teach programming language semantics to 4th year university students at the university of Nice. Here are course notes (in French).

Starting in the fall of 2004, I also teach more advanced programming language semantics to 5th year university students at the university of Nice. Here are my course notes:

- Equivalence between Natural Semantics and Structural Semantics, (en PDF)
- Execution and mechanical treatement of Specifications, (en PDF)
- An example exercise for proofs of program transformations.
- Descriptions du parallélisme (en PDF),
- Describing a simple functional programming language (freely inspired from the paper by D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn "A Simple Applicative Language:{M}ini-{ML}", ACM Conference on Lisp and Functional Programming, 1986), Prolog sources
- The rest of the course uses directly the book of
Hanne Riis Nielson and Flemming Nielson,
*Semantics with Applications, a formal introduction*, John Wiley and Sons, 1992.

I also taught a course entitled "Introduction aux méthodes formelles" (introduction to formal methods). Here are my course notes:

- Introduction to Hoare logic (in French)
- Introduction to functional programming and proof (in French). For exercises I suggest using Laurent Théry's collection of exercises.
- Satisfiability and Binary Decision Diagrams

Yves Bertot Last modified: Fri Dec 3 14:29:19 MET 2004