Coq School 2013, Tsinghua

Jean-Jacques Lévy ( Tsinghua, 2013 )

5th Asian-Pacific Summer School on Formal Methods (August 5-10, 2013) (see web site for full program)

Class 1 Functions [Pdf, Pdf4]

Class 2 Data types (I) [Pdf, Pdf4]

Class 3 Data types (II) [Pdf, Pdf4]

Class 4 Polymorphism [Pdf, Pdf4]

Several references

Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions.
Yves Bertot, Pierre Casteran. Springer, pp. 497, 2004. ISBN: 978-3642058806.

Bibliography on lambda-calculus
Lambda-calculus and Programming (in French) [Pdf, Video]