Courses taught by Yves Bertot

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:

  1. Equivalence between Natural Semantics and Structural Semantics, (en PDF)
  2. Execution and mechanical treatement of Specifications, (en PDF)
  3. An example exercise for proofs of program transformations.
  4. Descriptions du parallélisme (en PDF),
  5. 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
  6. 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:

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

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