Semantics of Programming languages (2nd unit)

1. An introduction to Coq.
2. Equivalence between Natural Semantics and Structural Semantics
3. Execution and mechanical treatement of Specifications
4. 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
5. 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.

Previous exams and exercises.

6. An example exercise for proofs of program transformations.
7. An exercise in formal description of a language (exam of '04)
8. An exercise in the formal proofs of semantic properties (exam of '04)
9. An exercise in mechanical proof of semantics (exam of '04)
10. Solutions to the three exercises taken from the '04 exam (don't get too worried, students only had to complete one of the exercises to get full marks; also each solution contains some extra information, like Prolog programs or Coq proofs).
11. An exercice in the definition of a language with side-effects in expressions (exam of '05). and the solution
12. An exercise on proofs of transformation in the language of the course (exam of '06), and the solution
13. Lab. session in November 2006: proofs in semantics, including the proof of correctness for a loop transformation. The solution is voluntarily kept private, but I can mail it to you if you request it.
14. Lab.session in November 2005 and November 2007: proofs in semantics, including the proof of correctness of substitution transformation.
15. Another possible lab. session proof of completeness for the Structural operational semantics (little step) with respect to natural semantics (big step). The solution actually is in the course notes.

Student project

The work presented in this page should represent a work load of several days. Here again, the solution is not provided, but I can discuss the different issues by mail. This is the project proposed in 2007.