On a vu dans ce cours une sémantique opérationnnelle de Ocaml qui montre que le langage suit une stratégie d'appel par valeur.On a ensuite montré comment raisonner par induction bien fondée pour prouver la terminaison de programmes et des proprietés de programems par raisonnement équationnel. On a appliqué tout cela sur l'exemple de l'associativité de append, et la correction complète d'un programme qui implante le tri par insertion.
On a vu briévement ensuite les problèmes d'efficacité en temps et en espace.
