Useful informations for Guy Cousineau's lectures in Nanjing

The slides for the lectures (pdf)
The Web site for Objective Caml
The O'Reilly book for Objective Caml
The Web site for the Coq Proof Assistant
The implementation of caml in caml example
The tautology checker example
CAUTION: To use the last two files with Ocaml 3.06, you should first type the command:
# #load "camlp4o.cma"