Lambda calculus, types system, interpreter, compiler, rewriting, resolution... and some other maths I love
See the Tex document (in French), the compiled pdf doc
Contains OCAML, SCHEME, COQ and AGDA code
Please see the file BOOK/main.pdf
Have a happy reading !