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:
- 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